---
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.
altloc:
  - http://let.uvt.nl/general/people/rmuskens/pubs/classden.pdf
chapter: ~
commentary: ~
commref: ~
confdates: ~
conference: ~
confloc: ~
contact_email: ~
creators_id: []
creators_name:
  - family: Muskens
    given: Reinhard
    honourific: ''
    lineage: ''
date: 1997-01
date_type: published
datestamp: 2006-08-06
department: Computerlinguistik
dir: disk0/00/00/50/44
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 5044
fileinfo: /style/images/fileicons/application_postscript.png;/5044/1/classden.ps|/style/images/fileicons/application_pdf.png;/5044/2/classden.pdf
full_text_status: public
importid: ~
institution: Universitaet des Saarlandes
isbn: ~
ispublished: unpub
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: 'program semantics, denotational semantics, classical logic'
lastmod: 2011-03-11 08:56:33
latitude: ~
longitude: ~
metadata_visibility: show
note: ~
number: ~
pagerange: ~
pubdom: FALSE
publication: ~
publisher: ~
refereed: FALSE
referencetext: ~
relation_type: []
relation_uri: []
reportno: CLAUS 86
rev_number: 14
series: ~
source: ~
status_changed: 2007-09-12 17:06:35
subjects:
  - comp-sci-lang
  - phil-logic
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
thesistype: ~
title: Program Semantics and Classical Logic
type: techreport
userid: 6111
volume: ~
<script src="//archive-bar.soton.ac.uk/archive-bar.js"></script>