Lambda calculus

Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. Il a été le premier formalisme utilisé pour définir et  caractériser les fonctions récursives et donc il a une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing et du modèle de Herbrand-Gödel. Il a depuis été appliqué comme  langage de programmation théorique et comme métalangage pour  la démonstration formelle assistée par ordinateur. Le lambda-calcul peut être ou non typé.
Pour la suite, voir Wikipédia.org…