IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
Reference no #926   Download bibtex file Type :   Html | Bib | Both
    Created: 2007-12-12 11:31:19
926 Add to my selection
      AUTHOR = {Muskens, Reinhard},
      TITLE = {Program Semantics and Classical Logic},
      YEAR = {1997},
      MONTH = {January},
      NUMBER = {86},
      PAGES = {29},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS-Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {},
      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 Scott Induction holds in this new setting, prove soundness of a Hoare calculus relative to our semantics, give a direct calculus 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.},
      ANNOTE = {COLIURL : Muskens:1997:PSC.pdf}
Last modified: Thu October 16 2014 19:11:34         BibAdmin