lambda-calcul et types

Yves Bertot (1)

1 MARELLE - Mathematical, Reasoning and Software

Ces notes présentent successivement le lambda-calcul pur, le lambda-calcul simplement typé, les différentes formes de récursion typée, les types dépendants et leur utilisation en programmation et en logique

Mots clés: lambda-calcul; types; récursion

Domaines: Logique en informatique [cs.LO]

Yves Bertot. lambda-calcul et types. Ecole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006. ⟨inria-00083975⟩