Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory

Alexander Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationLogic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages287-298
Number of pages12
ISBN (Print)0-7695-1483-9
DOIs
Publication statusPublished - 2002

Fingerprint

Dive into the research topics of 'Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory'. Together they form a unique fingerprint.

Cite this