Program Semantics and Classical Logic

Muskens, Reinhard (1997) Program Semantics and Classical Logic. [Departmental Technical Report] (Unpublished)

Full text available as:



In the tradition of Denotational Semantics one usually lets program constructs take their denotations in reflexive domains, i.e. in domains where self-application is possible. For the bulk of programming constructs, however, working with reflexive domains is an unnecessary complication. In this paper we shall use the domains of ordinary classical type logic to provide the semantics of a simple programming language containing choice and recursion. We prove that the rule of {\em Scott Induction\/} holds in this new setting, prove soundness of a Hoare calculus relative to our semantics, give a direct calculus ${\cal C}$ on programs, and prove that the denotation of any program $P$ in our semantics is equal to the union of the denotations of all those programs $L$ such that $P$ follows from $L$ in our calculus and $L$ does not contain recursion or choice.

Item Type:Departmental Technical Report
Keywords:program semantics, denotational semantics, classical logic
Subjects:Computer Science > Language
Philosophy > Logic
ID Code:5044
Deposited By: Muskens, Dr Reinhard
Deposited On:06 Aug 2006
Last Modified:11 Mar 2011 08:56


Repository Staff Only: item control page