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