Events

22 April 2009

Wednesday, April 22, 2009, 11h, bdg I, 1st floor,
the MSR-INRIA Joint Centre,
Inria Saclay,

Models and theories of lambda calculus
Giulio Manzonetto,
INRIA

A quarter of century after Barendregt’s main book, a wealth of interesting problems concerning denotational models and equational theories of the pure untyped lambda calculus are still open. In this talk we will see some of these problems and some techniques that have been recently developed to attack these problems.

The models of lambda calculus have been considered for longtime as algebraically pathological. In this talk we will see that this common belief is false. By generalizing to universal algebra concepts originating from lambda calculus and programming we will define the general class of Church algebras that includes all models of lambda calculus, all Boolean algebras, all Heyting algebras, all rings with unit, etc. We will see that Church algebras enjoy good algebraic properties (like a Stone’s representation theorem) that lead us to interesting results concerning both the models and the theories of lambda calculus.
Finally, we will investigate a longstanding open problem proposed by Honsell in 1984: is there a continuous model of lambda calculus having lambda-beta or lambda-beta-eta as equational theory? We will define the class of `effective’ models of lambda calculus and we will see that for this class of models we are able to give a precise answer by using methods of recursion theory.