Formalizing synthetic domain theory - the basic definitions

Reus, Bernhard (1999) Formalizing synthetic domain theory - the basic definitions. Journal of Automated Reasoning, 23 (3-4). pp. 411-444. ISSN 01687433

Full text not available from this repository.

Abstract

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.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 20:10
Last Modified: 08 Nov 2013 14:33
URI: http://sro.sussex.ac.uk/id/eprint/24410
📧 Request an update