LAMBDA CALCULUS

Sandra Alves (University of Porto)

The λ-calculus is a Turing-complete model of computation that was first introduced by Church to serve as a foundational model for mathematics. Although the full system proved to be inconsistent, Church isolated the subsystem dealing only with functions that turnout to be a model for computable functions. This system is the λ-calculus as we known it today and has a fundamental role in the theory of programming languages, particularly functional programming languages like Haskell, ML and Scheme.

The λ-calculus, together with its reduction notions, can be seen as a particular case of a higher-order rewriting system. In this course we will explore the rewriting aspects of the λ-calculus. The course will be organised in four lectures that will include some time to practice some of the presented concepts. The lectures will be organised as follows:

• In the first lecture we will present the basic concepts of the λ-calculus: syntax; notions of reduction; reduction strategies; and properties of reduction
• The second lecture will be devoted to the expressive power of the λ-calculus: encodings of different data constructors and definability of total recursive functions
• In the third lecture we will explore some fundamental theorems of the λ-calculus
• The last lecture will focus on the typed λ-calculus, in particular the system of simple types and its properties