<> "The repository administrator has not yet configured an RDF license."^^ .
<> .
.
"Program Semantics and Classical Logic"^^ .
"In the tradition of Denotational Semantics one usually lets program\nconstructs take their denotations in reflexive domains, i.e. in domains\nwhere self-application is possible. For the bulk of programming\nconstructs, however, working with reflexive domains is an\nunnecessary complication. In this paper we shall use the domains\nof ordinary classical type logic to provide the semantics of a\nsimple programming language containing choice and recursion. We prove\nthat the rule of {\\em Scott Induction\\/} holds in this new setting, prove\nsoundness of a Hoare calculus relative to our semantics, give a\ndirect calculus ${\\cal C}$ on programs, and prove that the denotation of\nany program $P$ in our semantics is equal to the union of the denotations\nof all those programs $L$ such that $P$ follows from $L$ in our calculus\nand $L$ does not contain recursion or choice."^^ .
"1997-01" .
.
.
.
.
.
.
.
.
"Reinhard"^^ .
"Muskens"^^ .
"Reinhard Muskens"^^ .
.
.
.
.
.
"Program Semantics and Classical Logic (Postscript)"^^ .
.
.
.
.
.
"classden.ps"^^ .
.
.
"Program Semantics and Classical Logic (PDF)"^^ .
.
.
.
.
.
.
.
.
"classden.pdf"^^ .
.
.
"Program Semantics and Classical Logic (Image (PNG))"^^ .
.
.
.
.
.
"preview.png"^^ .
.
.
"Program Semantics and Classical Logic (Image (PNG))"^^ .
.
.
.
.
.
"preview.png"^^ .
.
.
"Program Semantics and Classical Logic (Indexer Terms)"^^ .
.
.
.
.
.
"indexcodes.txt"^^ .
.
"HTML Summary of #5044 \n\nProgram Semantics and Classical Logic\n\n" .
"text/html" .
.
.
"Language" .
.
.
"Logic" .
.