Proof Theory: Lambda Calculus

Italian Summer School of Logic 2005




Versione Italiana
Teacher:Stefano Berardi ( http://www.di.unito.it/~stefano/ , stefano.berardi adress: di.unito.it)
Course Notes: Available in the format: zipped ppt . Includes all exercises assigned to students (end of file). Solutions are available in format zipped ppt .

Aim of the Course:
This course introduces the lambda calculus as an abstract model of the notion of computation and of constructive proof. The goal is to make the student familiar with concepts like: definition unfolding, unicity of the result, completeness of a computation strategy, program equality. For a better understanding of the course can be useful, but are not required, the first notions of programming.

Program of the course:

  • 1. Introduction. The Lambda Calculus as a computational model for functional languages.
  • 2. Syntax of Lambda Calculus. alpha, beta-reductions. Normal form, normalization, strong normalization. COmputational strategy call-by-name and call-by-value.
  • 3. Main Theoretical Results. Head Normal Form, head reduction, leftmost reduction and completeness results. Theorems: Confluence and Church-Rosser. The theory of beta-conversion. Observational ordering and equality, solvable terms.
  • 4. Representing recursive maps. Natural Numbers and Booleans in the Lambda Calculus. Arithmetic on Church numerals. Recursive maps and fixed point operator.
  • 5. Simply Typed Lambda Calculus. Unification and Curry-Howard isomorphism between lambda terms and constructive proofs.

    Acknoledgements.
    This course expands a first course in Lambda Calculus, for undergraduate students, by Prof. Barbanera of Catania University, Italy. Barbanera's course (more basic) is available in the formats: html , pdf, together with the exercises: es1, es2. The last section of the course is taken from a lesson of Prof. H. Geuvers (Summer School of Logic and Type Theory, Eugene, Oregon, USA, 2002).
    We warmly thanks Prof. Barbanera and Prof. Geuvers for giving permission of using their material.

    Bibliography

  • Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics. 2d ed. North-Holland, 1984.
  • Barendregt, H. 1992. Lambda Calculi with Types. In: Abramsky, G., & Maibaum (eds), Handbook of Logic in Computer Science, vol. II. Oxford University Press. http://citeseer.ist.psu.edu/barendregt92lambda.html

    Stefano Berardi