[Prev][Next][Index][Thread]
Paper announcement
The following paper is now available over the Web.
Computational Adequacy for Recursive Types
in Models of Intuitionistic Set Theory
We present a general axiomatic construction of models of FPC,
a recursively typed lambda-calculus with call-by-value operational
semantics. Our method of construction is to obtain such models as
full subcategories of categorical models of intuitionistic set
theory. This allows us to obtain a notion of model that encompasses
both domain-theoretic and realizability models. We show that the
existence of solutions to recursive domain equations, needed for
the interpretation of recursive types, depends on the strength of
the set theory. The internal set theory of an elementary topos is
not strong enough to guarantee their existence. However, solutions
to recursive domain equations do exist if models of intuitionistic
Zermelo-Fraenkel set theory are used instead. We apply this result
to interpret FPC, and we provide necessary and sufficient conditions
on a model for the interpretation to be computationally adequate,
i.e. for the operational and denotational notions of termination
to agree.
http://www.dcs.ed.ac.uk/~als/Research/rec_adequacy.ps.gz
http://www.dcs.ed.ac.uk/~als/Research/rec_adequacy.pdf.gz
Alex
--
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209
URL: http://www.dcs.ed.ac.uk/home/als