1.10   Bibliographie

• [Chu41], Alonzo Church, ``The Calculi of lambda-conversion'', Princeton University Press

  Le l-calcul a été présenté par Alonzo Church dans cet ouvrage qui est un texte tout à fait lisible et utile pour comprendre les idées de base et les connections entre l-calcul, récursivité et théorie de la calculabilité.

• [Bar84], Barendregt, ``The lambda-calculus: its syntax and semantics'' North Holland,1984.

  est un peu la bible du l-calcul, mais c'est comme si c'était écrit en hébreu.

• [Hue89], Gérard Huet. "Initiation au l-calcul" Notes de cours du DEA Informatique Fondamentale (P7), 1989

  contient les démonstrations de base du l-calcul pur et typé en utilisant une syntaxe à la ML.

• [HS86], Hindley and Seldin.``Introduction to Lambda-Calculus and combinators'' Cambridge University Press,1986

  est une excellente introduction, qui traite très bien aussi le l-calcul typé.

• [Str77], Strachey, "Denotational Semantic", MIT Press, 1977

  Un texte théorique mais facile et important sur les liens entre l-calcul et informatique.

• [Par88], M. Parigot , "Preuves et Programmes : les Mathematiques comme Langage de Programmation", 1988, aperçu des mathématiques, (CNRS) 1988.

  Pour avoir un aperçu des liens entre logique et informatique, l'article de M. Parigot traite en huit pages du l-calcul, de la logique du 2ème ordre et de la logique linéaire.