An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC
View/ Open
Date
1994Author
Fiore, Marcelo P
Plotkin, Gordon
Metadata
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 non-trivial and 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.