A Stratified Semantics of General References Embeddable in Higher-Order Logic

Amal J. Ahmed, Andrew W. Appel, Roberto Virga

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


We demonstrate a semantic model of general references --- that is, mutable memory cells that may contain values of any (statically-checked) closed type, including other references. Our model is in terms of execution sequences on a von Neumann machine; thus, it can be used in a Proof-Carrying Code system where the skeptical consumer checks even the proofs of the typing rules. The model allows us to prove a frame-axiom introduction rule that allows locality of specification and reasoning, even in the event of updates to aliased locations. Our proof is machine-checked in the Twelf metalogic.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:31
Maintainer lics02@dcs.ed.ac.uk.
Start Conference Manager
Conference Systems