Lecture outline :
- Curry-Howard ;
- gentzen's natural deduction ;
- inductive definitions following Martin-Löf ;
- algebraic presentation of type theory and term model as initial model ;
- some examples of models, in particular the set model and prefix models.
