[Prev][Next][Index][Thread]

Posting for Types Bulletin Board

I have written two papers on the denotational semantics of types,
or more precisely, a long and short version of the same paper.
(The long version uses a richer illustrative language.)

These papers may be obtained From my web page at 

   http://www.cs.cmu.edu/~jcr

or by anonymous ftp:  

   Execute "ftp FTP.CS.CMU.EDU",
   enter "anonymous" as your name,
   enter your userid@host as your password,
   execute "cd /afs/cs/user/jcr/ftp",
   and read the file README.

They should soon be available from Hypatia at

   http://hypatia.dcs.qmw.ac.uk

The long version is also available at

   http://www.brics.dk/RS/00/32/

Reynolds, John C.
The Meaning of Types --- From Intrinsic to Extrinsic Semantics
BRICS Research Series RS--00--32, December 2000.
DAIMI, Department of Computer Science, University of Aarhus
filenames = "typemeaning.dvi.gz typemeaning.pdf typemeaning.ps.gz"

A definition of a typed language is said to be ``intrinsic''
if it assigns meanings to typings rather than arbitrary phrases, so that
ill-typed phrases are meaningless.  In contrast, a definition is said
to be ``extrinsic'' if all phrases have meanings that are independent
of their typings, while typings represent properties of these meanings.
For a simply typed lambda calculus, extended with recursion,
subtypes, and named products, we give an intrinsic denotational semantics
and a denotational semantics of the underlying untyped language.  We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics.  From these results, we derive an extrinsic
semantics that uses partial equivalence relations.

A definition of a typed language is said to be ``intrinsic'' if it assigns
meanings to typings rather than arbitrary phrases, so that ill-typed phrases
are meaningless.  In contrast, a definition is said to be ``extrinsic''
if all phrases have meanings that are independent of their typings, while
typings represent properties of these meanings.

For a simply typed lambda calculus, extended with recursion, subtypes,
and named products, we give an intrinsic denotational semantics and a
denotational semantics of the underlying untyped language.  We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics.  From these results, we derive an
extrinsic semantics that uses partial equivalence relations.


John C. Reynolds
What do Types Mean? --- From Intrinsic to Extrinsic Semantics
To appear in Essays on Programming Methodology, edited by Annabelle McIver
and Carroll Morgan, to be published by Springer-Verlag, New York, 2001.
filenames = "shorttypemeaning.dvi.gz shorttypemeaning.ps.gz"

A definition of a typed language is said to be ``intrinsic'' if it
assigns meanings to typings rather than arbitrary phrases, so that ill-typed
phrases are meaningless.  In contrast, a definition is said to be 
``extrinsic'' if all phrases have meanings that are independent of their
typings, while typings represent properties of these meanings.

For a simply typed lambda calculus, extended with integers, recursion, and
conditional expressions, we give an intrinsic denotational semantics and a
denotational semantics of the underlying untyped language.  We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics.  From these results, we derive an extrinsic
semantics that uses partial equivalence relations.