La théorie des types et ses applications à la Science des ordinateurs

https://pdfs.semanticscholar.org/7f8b/cb79306cd0d1e5870b5f0b8038c3c94983fd.pdf
La théorie des types émerge des travaux de Bertrand Russell , au début du 20eme siècle, elle atteint des niveaux plus sophistiqués dans les recherches de logiciens comme Alonso Chirch , HoTT en est le stade le plus moderne ( début du 21 éme siècle ) et constitue une nouvelle manière de fonder toutes les mathématiques.
HoTT (homotopy type theory) se situe au croisement de l’homotopie, de la théorie des ∞-catégories, de la logique mathématique et de la Science des ordinateurs (“computer Science”).
L’article suivant fait le point sur ces applications pratiques:

https://pdfs.semanticscholar.org/7f8b/cb79306cd0d1e5870b5f0b8038c3c94983fd.pdf

Dans ce blog nous en resterons aux mathématiques, mais il est important d’être au courant des applications en informatique.

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, Homotopy, homotopy type theory and tagged , , . Bookmark the permalink.