Department of Computer and Information
Science
Università di Genova
4pm 2 September 2003
Room 2511, JCMB, King's Buildings
We present a parametric domain-theoretic model for the polymorphic lambda-calculus with a fixed-point operator. The model is relationally parametric in the sense of Reynolds and the notions of domain and relation come from Synthetic Domain Theory.
In order to explain the properties of the model, we review the construction of parametric models for the polymorphic lambda-calculus and then adapt it along the lines suggested by works of Amadio and Plotkin.
We also suggest how to obtain the model as a purely synthetic construction.
This is work in progress, jointly with Lars Birkedal and Rasmus Mogelberg at ITU (Copenhagen).