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

Palmse, Estonia, February 28 - March 4, 2016

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

Valid CSS! Valid XHTML 1.0 Strict Last changed May 7, 2016 12:49 Europe/Tallinn (GMT +03:00) by local organizers, ewscs16(at)cs.ioc.ee
EWSCS'16 page: http://cs.ioc.ee/ewscs/2016/