## Paper: Domain Theory in Logical Form (at LICS 1987)

*Winner of the Test-of-Time Award in 2007***Samson Abramsky**

### Abstract

A metalanguage for denotational semantics is given a logical interpretation: types are interpreted as propositional theories; terms (in an extended typed λ-calculus, denoting elements of types) are embedded in an endogenous program logic, which characterises their behaviour in terms of which properties they satisfy; terms (in an extension of the algebraic metalanguage of cartesian closed categories, denoting morphisms between types) are embedded in an exogenous logic, which characterises their behaviour as predicate transformers or modal operators. This interpretation is related to the standard domain-theoretic one via the machinery of Stone duality, and an exact correspondence is obtained. Some applications to logics for specific computational situations (e.g. concurrency) are mentioned.

### BibTeX

@InProceedings{Abramsky-DomainTheoryinLogic, author = {Samson Abramsky}, title = {Domain Theory in Logical Form}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {47--53}, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }