#HoTT Théorie homotopique des types et programmation

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

Advertisements
This entry was posted in Computer science, homotopy type theory. Bookmark the permalink.