INFO4213 : Preuves et programmes
Programs and proofs
- Responsable(s) :
-
- Daniel Hirschkoff
- Enseignant(s) :
-
- Michele Angelo Pagani
Niveau
M1+M2
Discipline
Informatique
Public externe (ouverts aux auditeurs de cours)
Informations générales sur le cours : INFO4213
These lectures introduce the Curry-Howard correspondence between proofs and programs, illustrating some of its key benefits.
We present the natural deduction system for both intuitionistic and classical logic, discussing the properties and limitations of these systems.
Furthermore, we establish a correspondence with the simply typed Lambda-Calculus and some of its extensions, such as the Lambda Mu-Calculus for classical natural deduction and System F for second-order propositional logic.
We will also prove some theorems that highlight the elegance of this correspondence, including the normalization and the parametricity theorems for System F.
A basic understanding of lambda calculus and logic is recommended, as well as an elementary familiarity with the Coq proof assistant. These concepts are introduced, for example, in the L3 year of the Computer Science Department of ENS de Lyon: "Theory of Programming" and "Introduction to Logic". Familiarity with functional programming is also helpful for appreciating certain use cases.
2 hours of lectures per week, and 2 hours of lab session per week. Some practical sessions will also be offered to formalise concepts introduced in lectures using the Coq proof assistant.
TBA