File(s) not publicly available
Formalizing synthetic domain theory - the basic definitions
Synthetic Domain Theory (SDT) is a constructive variant of Domain Theory where all functions are continuous following Dana Scott's idea of "domains as sets". Recently there have been suggested more abstract axiomatizations encompassing alternative notions of domain theory as, for example, stable domain theory. In this article a logical and axiomatic version of SDT capturing the essence of Domain Theory à la Scott is presented. It is based on a sufficiently expressive version of constructive type theory and fully implemented in the proof checker LEGO. On top of this "core SDT" denotational semantics and program verification can be - and in fact has been - developed in a purely formal machine-checked way. The version of SDT we have chosen for this purpose is based on work by Reus and Streicher and can be regarded as an axiomatization of complete extensional PERs. This approach is a modification of Phoa's complete ¿-spaces and uses axioms introduced by Taylor.
History
Publication status
- Published
Journal
Journal of Automated ReasoningISSN
01687433Publisher
SpringerExternal DOI
Issue
3-4Volume
23Page range
411-444ISBN
0168-7433Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC