 BBB classroom.
 Lecturers:
 Tutorials by Étienne Miquey.
Overview
The objective of this course is to provide the basics of the theory underlying the Coq proof assistant,
namely the CurryHoward correspondence between proofs and programs.
Technically, we will investigate intuitionistic logics and their relations to typed λcalculi.
Prerequisites:

We assume some familiarity with computability theory and mathematical logic,
essentially
corresponding to the courses Fondements de l'informatique and Logique given in the
L3 year of the Computer Science Department of ENS de Lyon.
Bibliography:

The course is loosely based on the reference book:

Sørensen, M. H. et Urzyczyn, P.,
Lectures on the CurryHoward Isomorphism,
volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Sørensen, M. H. et Urzyczyn, P.,
Lectures on the CurryHoward Isomorphism,
Back home.