RE: types as set of values

To: "'Uwe.Nestmann@epfl.ch'" <Uwe.Nestmann@epfl.ch>, Giuseppe Castagna <Giuseppe.Castagna@ens.fr>
Subject: RE: types as set of values
From: Robert Harper <Robert.Harper@cs.cmu.edu>
Date: Thu, 3 Apr 2003 11:04:04 -0500
Cc: types@cis.upenn.edu

Martin-Loef's Constructive Mathematics and Computer Programming is founded
on the notion of the canonical forms of a type, which would correspond to
the values of that type in a PL setting.  Roughly speaking, a type is
defined by the canonical forms that inhabit it (and by what counts as
equality between them).  A variant of this semantics was used as the basis
for the NuPRL type theory.  The formulation of type safety as
progress+preservation is also based on this conception of type; the crux of
the progress lemma is to identify the canonical forms of each type.

Bob Harper

-----Original Message-----
From: Uwe.Nestmann@epfl.ch [mailto:Uwe.Nestmann@epfl.ch]
Sent: Thursday, April 03, 2003 9:45 AM
To: Giuseppe Castagna
Cc: types@cis.upenn.edu
Subject: Re: types as set of values


[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

>>>>> "GC" == Giuseppe Castagna <Giuseppe.Castagna@ens.fr> writes:

GC>    interpreting a type of a language as the set of the _values_ of the
GC> language that have that type is an idea that belongs to the type
GC> folklore. I am trying to trace back this idea, and the oldest paper I
GC> was able to find that mentions it is the Amadio and Cardelli paper on
GC> subtyping recursive types, but I am pretty sure that older references
GC> must exist. Has anyone a better (i.e. older) reference?


You find links to older references on
http://doi.acm.org/10.1145/512927.512938
of the paper "Types are not sets" :-)


One by Reynolds apparently of 1969 ...


== Uwe ==