Module LA : Certification de programmes et lambda-calcul

Module LA : Certification de programmes et lambda-calcul

Equipe pédagogique :

Frederic Prost

Volume :

12h.

Spécialité :

S&L

Les liens entre la logique et l'informatique sont historiques. C'est en travaillant sur les résultats d'incomplétudes de Gödel que Turing en est arrivé aux concepts théoriques servant de base aux ordinateurs actuels. L'étude de ces liens entre la logique et l'informatique permet de considérer simultanément ces deux aspects. Prouver des propriétés sur un programme par exemple, suppose de pouvoir lier une logique (la preuve) avec un système de programmation. Habituellement, la preuve se fait une fois le programme construit. Dans ce cours nous montrons comment la construction d'un programme et la preuve de ses propriétés peut se faire simultanément au sein d'un même formalisme.

Ce cours se déroule autour du modèle du lambda-calcul qui, dans une première partie, sera étudié en tant que tel comme modèle de calcul Turing-équivalent. Dans une seconde partie, nous montrons comment le typage du lambda-calcul permet de faire le lien direct entre la logique et le calcul. Notamment comment l'isomorphisme de Curry-Howard permet d'extraire des programmes certifiés à partir de démonstrations et comment on peut lier l'activité de programmation et celle de certification. Finalement, nous traitons des différents systèmes de typages (polymorphisme, types dépendants, ordres supérieurs) et exhibons leurs liens respectifs tout en montrant quelles sont les répercussions en termes de certification.

Connaissances / Méthodes acquises :

• Fondement de la théorie de la preuve.
• Lambda calcul comme modèle de calcul.
• Informatique vue comme le pendant opératoire de la logique.
• Démonstration par induction structurelle (termes et types).

Module LA : Certification de programmes et lambda-calcul