[bemus@THEORY.LCS.MIT.EDU: TOC Seminar -- TOMORROW, January 7, 1987 -- Kurt Sieber]

• To: types@THEORY.LCS.MIT.EDU, logic@THEORY.LCS.MIT.EDU
• Subject: [bemus@THEORY.LCS.MIT.EDU: TOC Seminar -- TOMORROW, January 7, 1987 -- Kurt Sieber]
• From: Albert R. Meyer <meyer@THEORY.LCS.MIT.EDU>
• Date: Thu, 7 Jan 88 17:03:28 est

PREVIEW OF POPL TALK:

Date: Wed, 6 Jan 88 16:10:28 est
From: Sally C. Bemus <bemus@THEORY.LCS.MIT.EDU>
To: theory-seminars@THEORY.LCS.MIT.EDU
Subject: TOC Seminar -- TOMORROW, January 7, 1987 -- Kurt Sieber

			DATE:    Thursday, January 7, 1987
			TIME:    Refreshments: 2:45PM
			LECTURE: 3:00PM
			PLACE:   NE43-512A

	    REASONING ABOUT LOCAL VARIABLES ALGOL-LIKE PROCEDURES

				 Kurt Sieber
			    Univ. des Saarlandes

We improve the usual denotational semantics for local variables to obtain a
"store-model" semantics which exactly captures (is "fully abstract for)
operational semantics of Algol-like procedures with first-order parameters
(call by reference).  Some simple facts about the behavior of local variables
in procedures with procedure parameters are then shown to be independent of
essentially all known program verification systems by observing that although
store models (1) agree with the operational semantics of completely declared
programs, and (2) all known proof rules for reasoning about programs are
sound for store models, nevertheless (3) some of the simple facts which are
true operationally are false on store models.  We then discuss methods for
constructing semantical models which justify stronger proof principles, using
various categories of functors into cpo domains.

HOST: Prof. Albert R. Meyer

• Next: [goguen@csl.sri.com: higher order functions considered unnecessary]
• Index(es):
  • Main
  • Thread