#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.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s