Lecture 1: Introduction
Teachers: Bruno Barras & Matthieu Sozeau
Proof assistants (M2 MPRI)
Lecture 2: Martin-Löf’s Type Theory, System F, Calculus of Constructions
Teachers: Bruno Barras & Matthieu Sozeau
Lecture 3: Inductive Types
Teacher: Bruno Barras
Lecture 4: Models
Teacher: Bruno Barras