We present a simple and workable axiomatization of domain theory within intuitionistic set theory, in which predomains are (special) sets, and domains are algebras for a simple equational theory. We use the axioms to construct a relationally parametric set-theoretic model for a compact but powerful polymorphic programming language, given by a novel extension of intuitionistic linear type theory based on strictness. By applying the model, we establish the fundamental operational properties of the language. 1.
|Number of pages||10|
|Publication status||Published - 2004|