Plan du cours :
- Curry-Howard ;
- déduction naturelle de Gentzen ;
- définitions inductives suivant Martin-Löf ;
- présentation algébrique de la théorie des types et modèle des termes comme modèle initial ;
- quelques exemples de modèles, en particulier modèle ensembliste et modèles de préfaisceaux.
