[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.