An axiomatisation of computationally adequate domain theoretic models of FPC

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