DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Parametric polymorphism in intuitionistic / linear lambda-calculus as a setup for axiomatic domain theory

Rasmus Ejlers Møgelberg,
Universita degli Studi di Genova

Thursday, December 15, 15:15-16:00
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 4

Abstract:

More than ten years ago Gordon Plotkin suggested using a dual intuitionistic / linear lambda calculus with fixed points and parametric polymorphism (PILLY) as a setup for axiomatic domain theory, because parametric polymorphism in combination with fixed points gives solutions to recursive domain equations. Development of this syntactic theory and a category theoretic account of models of the theory was the topic of my PhD dissertation, and was done in collaboration with Lars Birkedal and Rasmus Lerchedahl Petersen.

In this work I test Plotkin's thesis that the theory is a useful approach to axiomatic domain theory, by adapting to this setting one of the main achievements of domain theory, namely sound and computationally adequate semantics for FPC, a simply typed lambda calculus with sum types, fixed points and general recursive types, with respect to a call-by-value operational semantics.

In this talk I will show how to give a sound and computationally adequate interpretation of a variant of FPC with polymorphism (PolyFPC) into PILLY and sketch how this result can be used to prove operational results - in particular consequences of parametricity - for PolyFPC. The main technical problems we need to solve on the way come from interpreting the intuitionistic type theory PolyFPC into the linear part of PILLY.

The talk will contain a brief introduction to PILLY, and no prior knowledge of parametricity is needed.

Scientific host: Lars Birkedal. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org