Résumé
Le premier cours a retracé les trois chemins qui mènent à la découverte de Curry et Howard : le lambda-calcul, la logique intuitionniste, et les systèmes de types simples.
Vers 1930, Church introduit la lambda-notation λx.e pour désigner la fonction qui à x associe e, et l’utilise pour unifier diverses notations mathématiques faisant intervenir des variables liées (sommes, limites, quantificateurs, etc.). Son premier lambda-calcul, publié en 1932 et 1933, est une logique mathématique qui utilise la lambda-notation pour représenter les ensembles. Cette logique est rapidement abandonnée car incohérente. En revanche, débarrassé de ses connecteurs logiques, le lambda-calcul pur s’impose dès 1936 comme un formalisme fondamental de la calculabilité, en équivalence avec les machines de Turing, puis, dès le langage Lisp (1960), comme noyau des langages fonctionnels de programmation.
La logique intuitionniste, introduite par Glivenko et Heyting vers 1928, formalise la notion de démonstration constructive, qui est un aspect important de l’intuitionnisme, la philosophie des mathématiques fondée par Brouwer. Suivant l’interprétation BHK (Brouwer, Heyting, Kolmogorov) de l’intuitionnisme, les seules propositions vraies en logique intuitionniste sont celles qui sont justifiées par une construction, c’est à dire un objet mathématique qui atteste de leur véracité. Ainsi, une construction de ∃x.P est une paire d’une valeur pour x et d’une construction de P(x). Les démonstrations non constructives de ∃x.P sont donc exclues.
