Semantic Types : A fresh look at the ideal model for types

Jérôme Vouillon

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types as a solution of a fixpoint does not rely on metric spaces properties, but instead uses the fact that the identity is the limit of projection terms. This establishes a connection with the work of Pitts on relational properties of domains. We suggest that the right generalization of ideals are closed sets of terms defined by orthogonality with respect to a set of contexts.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Start Conference Manager
Conference Systems