"Une introduction à la théorie homotopique des types", par Aurélien Alvarez (13 avril 2016)
mise en page : S. Dugowson
Titre humoristique de l'exposé d'Aurélien Alvarez :
Un jeu vidéo pour adultes et une thématique HoTT !
Questions
Lors de la discussion, les travaux de Francis Sergeraert ont été mentionnés par Alain Prouté. Voir par exemple la vidéo suivante :
Francis Sergeraert (Institut Fourier) : "Effectivité en Topologie Algébrique face à Gödel"
Références
HoTT
HoTT, le bouquin, le blog, etc. : https://homotopytypetheory.org
HoTT + COQ
ERC CoqHoTT : http://web.emn.fr/x-info/ntabareau/coqhott/
une très bonne référence pour qui veut apprendre HoTT et Coq en même temps : http://arxiv.org/pdf/1210.5658v1.pdf
le logiciel Coq : https://coq.inria.fr
Aurélien Alvarez
http://www.univ-irem.fr/IMG/pdf/arelien_alvarez_toulouse_04-06-2015.pdf
Coqito ergo sum : http://images.math.cnrs.fr/Coqito-ergo-sum
Antoine Chambert-Loir
"A la croisée des fondements des mathématiques, de l'informatique et de la topologie", 7 décembre 2013 :
Thierry Coquand
"logic and topology" (novembre 2015, IHES)
séminaire Bourbaki du 26 juin 2014 : https://www.youtube.com/watch?v=T_WcQpj-2to
séminaire d’histoire du 16 janvier 2015 : https://www.youtube.com/watch?v=APY6mXN9MzM