On présente la syntaxe et la notion de réduction du lambda calcul. On présente les résultats de base (confluence, différents types de normalisation) ainsi que les différents codages de base pour les constructions usuelles. On introduit enfin les types simples et les règles de typage dans le cas du lambda calcul avec produits et on esquisse l'isomorphisme de Curry-Howard.