# Program Semantics and Classical Logic

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

Full text available as:

 Preview
Postscript
333Kb
 Preview
PDF
232Kb

## Abstract

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 program semantics, denotational semantics, classical logic Computer Science > LanguagePhilosophy > Logic 5044 Muskens, Dr Reinhard 06 Aug 2006 11 Mar 2011 08:56