creators_name: Muskens, Reinhard type: techreport datestamp: 2006-08-06 lastmod: 2011-03-11 08:56:33 metadata_visibility: show title: Program Semantics and Classical Logic ispublished: unpub subjects: comp-sci-lang subjects: phil-logic full_text_status: public keywords: program semantics, denotational semantics, classical logic 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. date: 1997-01 date_type: published institution: Universitaet des Saarlandes department: Computerlinguistik refereed: FALSE citation: Muskens, Reinhard (1997) Program Semantics and Classical Logic. [Departmental Technical Report] (Unpublished) document_url: http://cogprints.org/5044/1/classden.ps document_url: http://cogprints.org/5044/2/classden.pdf