Proofs and Programs

M1 IF course, ENS de Lyon.

Overview


The objective of this course is to provide the basics of the theory underlying the Coq proof assistant,
namely the Curry-Howard correspondence between proofs and programs.

Technically, we will investigate intuitionistic logics and their relations to typed λ-calculi.


Prerequisites:


Bibliography:

Homeworks



Courses












Valid XHTML 1.0 Strict



Back home.