Bibliothèque Tangente. N° 55. Une preuve de maths est un programme informatique ! p. 138-142.
Auteurs : Nguyen Le Than Dung ; Ledent Jérémy
Résumé
A la fin des années 1960 émerge l’idée qu’une preuve mathématique correspond à un programme informatique. On rêve ainsi de comprendre les programmes sous-jacent à toutes les démonstrations mathématiques. La « correspondance preuves-programmes » permet de concevoir des langages de programmation où les programmes sont mathématiquement prouvés sans bugs. Cet article présente les recherches menées au 20e siècle, celles-ci aboutissent à la théorie des types qui offre des connexions inattendues avec la topologie algébrique et la théorie des catégories.
Notes
Cet article est publié sous la rubrique « Savoirs ».
Il fait partie du dossier : Les apports de l’informatique dans Bibliothèque Tangente n° 55 – Les démonstrations.
Données de publication
Éditeur Editions POLE Paris , 2015 Collection Bibliothèque Tangente Num. 55 Format 17 cm x 24 cm, p. 138-142
ISBN 2-84884-198-2 EAN 9782848841984 ISSN 2263-4908
Public visé élève ou étudiant, enseignant, tout public Niveau 1re, 2de, licence, lycée, terminale Âge 15, 16, 17, 18, 19
Type chapitre d’un ouvrage, vulgarisation, popularisation Langue français Support papier
Classification