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.