#HoTT Théorie homotopique des types et programmation

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

La théorie homotopique des types a deux versants : l’un théorique, tourné vers le haut, celui de la théorie des types , celui que l’on trouve dans le Livre que nous étudions ici :

The HoTT Book

et l’autre tourné vers les applications, la programmation, qui dans HoTT joue un rôle important, notamment dans les « computer-checked proofs ». Le lien suivant porte justement sur l’expression dans un langage de programmation des notions théoriques (types, familles de types ou fibrations, produits, type vide, type unité,à un point, type des entiers naturels, etc..):

https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Bonn_talk_coq.pdf

View original post

Publicités