An axiomatisation of computationally adequate domain theoretic models of FPC

Abstract

Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domain-theoretic models of FPC are axiomatised and a wide subclass of them-the absolute ones-are proved to be both computationally sound and adequate. Examples include: the category of cpos and partial continuous functions and functor categories over it.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>