Axiomatic Domain Theory in Categories of Partial Maps
Axiomatic categorical domain theory is crucial for understanding the meaning of programs and reasoning about them. This book is the first systematic account of the subject and studies mathematical structures suitable for modelling functional programming languages in an axiomatic (i.e. abstract) setting. In particular, the author develops theories of partiality and recursive types and applies them to the study of the metalanguage FPC; for example, enriched categorical models of the FPC are defined. Furthermore, FPC is considered as a programming language with a call-by-value operational semantics and a denotational semantics defined on top of a categorical model. To conclude, for an axiomatisation of absolute non-trivial domain-theoretic models of FPC, operational and denotational semantics are related by means of computational soundness and adequacy results. To make the book reasonably self-contained, the author includes an introduction to enriched category theory.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
admissible monos algebraically compact categories algebraically complete Assume AXIOM axiomatic axiomatisation bifunctor binary categories of domains category of partial category of total characterisation coalgebra colimiting in AC colimits of w-chains composition computational cone coproducts Corollary counit Cpo-algebraic completeness Cpo-functor defined Definition denotational semantics diagram domain structure domain theory domain-theoretic models elim(e endofunctor example exists a unique F h e final coalgebra fixed-point operator follows forgetful functor h e2 inductive types initial algebra initial object intro(u J H L lifting functor Limit/Colimit Coincidence Theorem lubs of w-chains model of FPC monotone morphism natural isomorphism natural transformation notion of approximation pair parameterised V-algebraically partial cartesian closed partial maps pCpo Peter Freyd PKind Poset Poset-category Poset-enriched PROOF Proposition 4.3.3 pullback recursive types representation right adjoint terminal object total maps type constructors uniform upper-closed V-CAT V-category V-functor F V-natural w-chains of embeddings zero object