LTG Logic and Theory Group

• Wednesday, 15-18 (2h lectures, 1h exercises)

Lecture Room A97
Gebäude der Exakten Wissenschaften ("ExWi Building")
Sidlerstrasse 5

Arguably, the (untyped) lambda calculus is the simplest programming language in which all computable number-theoretic functions can be represented and evaluated. It is based on two elementary concepts only: application and abstraction. The lambda calculus provides the abstract foundations of all functional programming languages (e.g., Lisp, Scheme, Haskell).

The first part of these lectures is about the untyped lambda calculus. We introduce its syntax and semantics, discuss a series of data types within this framework, and study some central properties (for example: fixed-point theorem, Church-Rosser theorem). Later we present applicative structures and applicative theories as possible axiomatic alternatives.

Time permitting, we will also briefly turn to the simply-typed lambda calculus, its connections to propositional logic, and the famous Curry-Howard isomorphism.

This lecture is well suited for students who are interested in logic and in the
foundations of mathematic and/or computer science. It provides an introduction into a
research topic which has been actively pursued in the Bern group during the previous
years.

Basic knowledge in mathematical logic and/or theoretical computer science.

To be announced.