An axiomatic treatment of synthetic domain theory is presented, in the framework of the internal logic of an arbitrary topos. We present new proofs of known facts, new equivalences between our axioms and known principles, and proofs of new facts, such as the theorem that the regular complete objects are closed under lifting . In Sections 2–4 we investigate models, and obtain independence results. In Section 2 we look at a model in de Modified realizability Topos, where the Scott Principle (...) fails, and the complete objects are not closed under lifting. Section 3 treats the standard model in the Effective Topos. Theorem 3.2 gives a new characterization of the initial lift-algebra relative to the dominance. We prove that in the standard case it is not the internal colimit of the chain 0 → L → L 2 → ⋯ . The models in Sections 2 and 3 compare via an adjunction. Section 4 discusses a model in a Grothendieck topos. A feature here is that N is not well-complete , whereas 2 is. (shrink)

This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, (...) as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo–Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an “internal” computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine “external” computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC. In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models. (shrink)