The Lambda-Calculus, from Minimal to Classical Logic (Advanced course)
ESSLLI 2025 Summer School (Bochum, Germany)

Teachers: Davide Barbarossa, Giulio Guerrieri

Date: 28/07/2025 – 01/08/2025

Time: 5.00pm – 6.30pm

Room: HGB 40

You can also look at the schedule.

In this course we are going to gently investigate one of the key concepts of computer science,
namely that of (functional) programming language. In particular, we are going to stress its
theoretical foundations and (a small amount of) its relations with (a small part of) mathematical logic.
The main theme is the notion of computation, in its mathematical shape, and how it enlighten
the understanding of logic. We cover some classic topics of theoretical computer science and
mathematical logic (developed around the '70) with, at the end of the course, a very brief introduction
to one – among infinitely many – modern research topic conceptually following from those investigations.

• Lecture 1: Topology/domain-theory of the "graph model" over ℘(N): Notes1, Slides1

• Lecture 2: The λ-calculus: Notes2, Slides2

• Lecture 3: Category theory for denotational semantics: Slides3

• Lecture 4: Curry-Howard for minimal logic: Slides4

• Lecture 5: Krivine's approach to classical logic: Notes5, Slides5

Page maintained by Davide Barbarossa