Science informatique et logique mathématiques sont historiquement reliées: Alan Turing, John von Neumann, Alonzo Church et bien d'autres pionniers de l'informatique étaient des logiciens de formation ou de métier. Le cours 2018-2019 de la chaire Sciences du logiciel a étudié un autre lien, de nature mathématique celui-là (il s’agit d’un isomorphisme), entre langages de programmation et logiques mathématiques. Dans cette approche, démontrer un théorème, c’est la même chose que d’écrire un programme ; énoncer le théorème, c’est la même chose que de spécifier le type du programme.
Cette correspondance entre démonstration et programmation a d’abord été observée dans un cas simple par deux logiciens : Curry en 1958, puis Howard en 1969. Le résultat semblait tellement anecdotique que Howard ne l’a jamais soumis à une revue, se contentant de faire circuler des photocopies de ses notes manuscrites. Rarement photocopie a eu un tel impact scientifique, tant cette correspondance de Curry-Howard est entrée en résonance avec le renouveau de la logique et l’explosion de l’informatique théorique des années 1970 pour s’imposer dès 1980 comme un lien structurel profond entre langages et logiques, entre programmation et démonstration.
Aujourd’hui, il est naturel de se demander quelle est la « signification logique » de tel ou tel trait de langage de programmation, ou encore quel est le « contenu calculatoire » de tel ou tel théorème mathématique (c’est-à-dire, quels algorithmes se cachent dans sa démonstration ?). Plus important encore, la correspondance de Curry-Howard a débouché sur des outils informatiques comme Coq et Agda, qui sont à la fois des langages de programmation et des logiques mathématiques, et s’utilisent aussi bien pour écrire et vérifier des programmes que pour énoncer et aider à démontrer des théories mathématiques.
Le cours a retracé ce bouillonnement d’idées à la frontière entre logique et informatique, et mis l’accent sur les résultats récents et les problèmes ouverts dans ce domaine. Le séminaire a donné la parole à sept experts du domaine pour des approfondissements et des points de vue complémentaires.
Les enregistrement vidéo sont disponibles sur le site du Collège de France.
Les exposés étaient en français. Les enregistrements vidéo et les présentations sont disponibles sur le site du Collège de France.
Xavier.Leroy@college-de-france.fr