Quadrature. N° 103. p. 11-17. Un jeu vidéo pour adultes et une thématique HoTT !
Auteur : Alvarez Aurélien
Résumé
Une nouvelle thématique de recherche est en pleine effervescence ces dernières années, la théorie homotopique des types, à la croisée entre mathématiques, informatique théorique et logique. Le sujet est véritablement intriguant, d’autant qu’il interroge jusqu’aux fondements des mathématiques, directement en lien avec un autre sujet qui, lui, a des retombées jusque dans l’industrie : la certification de preuves et de programmes. Dans ce texte, l’auteur présente le logiciel Coq et donne quelques idées et pistes de lecture à propos de ces mathématiques tout à fait passionnantes et quelque peu déroutantes.
Notes
Quadrature est un magazine de mathématiques pures et appliquées. Il
s’adresse aux enseignants, étudiants, ingénieurs et amateurs de
mathématiques.
Tout internaute peut acheter le numéro en cours et les anciens numéros sur la site de la revue quadrature.info (ISSN de l’édition électronique : 1760-4826).
Une version texte intégral est en téléchargement sur le site https://www.aurelienalvarez.org/my-app/dist/papers
Données de publication
Éditeur Quadrature Revigny-sur-Ornain , 2017 Format A4, p. 11-17 Index Bibliogr. p. 17-17
ISSN 1142-2785
Public visé élève ou étudiant, enseignant, tout public Niveau licence Âge 18, 19, 20
Type article de périodique ou revue, vulgarisation, popularisation Langue français Support papier
Classification