21^st Estonian Winter School in Computer Science (EWSCS)
XXI Eesti Arvutiteaduse Talvekool

Herman Geuvers

Institute for Computing and Information Science
Radboud University Nijmegen
The Netherlands

The power of lambda calculus and types

Abstract

We will treat the lambda calculus as a language for computations and as a language for proofs. First we will look into the untyped lambda calculus, how one can represent data and functions in it and how undecidability phenomena (the halting problem) arise in it.

Then we will move on to typed lambda calculus and show how types on the one hand limit the expressiveness of the calculus (fewer lambda terms are allowed) but on the other hand enhance the expressiveness, because type information is added.

We will see that types are interesting in themselves. If we have dependent types, a type can express the full functional specification of a program, or a type can be seen as a formula with the lambda term being the proof of the formula. This follows from the well-known Curry-Howard formulas-as-types isomorphism that we will discuss.

Course materials

• H. Geuvers. The power of lambda calculus and types. Slides from the EWSCS 2016 course.
• Introduction [pdf]
• Lecture 1: Combinatory logic and lambda-calculus [pdf]
• Lecture 2: Self-interpretation in the lambda-calculus [pdf]
• Exercises 1 [pdf]
• Solutions to Exercises 1
• Lecture 3: Typed lambda-calculus and the Curry-Howard isomorphism [pdf]
• Lecture 4: Inductive types, proof assistants, homotopy type theory [pdf]
• Videos from the lectures.
• Lecture 1 [mp4]
• Lecture 2 [mp4]
• Lecture 3 [mp4]
• Lecture 4 [mp4]


• R. Nederpelt, H. Geuvers. Type Theory and Formal Proof. Cambridge Univ. Press, 2014. [doi link]
• H. Geuvers. Introduction to type theory. In A. Bove, L. S. Barbosa, A. Pardo, J. S. Pinto, eds., Revised Tutorial Lecture Notes from LerNet ALFA Summer School on Language Engineering and Rigorous Software Development, v. 5520 of Lect. Notes in Comput. Sci., pp. 1-56. Springer, 2009. [doi link]
• H. Barendregt. Reflection: an ubiquitous universal mechanism. Lecture notes from Huygens lecture, 2009. [pdf]
• Sec 3-5
• The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Inst. of Advanced Study, 2013. [online version]
• Ch 1, Ch 2.1-2.4, 2.8-2.14, Ch 3.3-3.7, Ch 5.1-5.2, Ch 6.1-6.3, Ch 7.2

Last changed May 7, 2016 12:49 Europe/Helsinki (GMT +03:00) by local organizers, ewscs16(at)cs.ioc.ee
EWSCS'16 page: //cs.ioc.ee/ewscs/2016/