TY - JOUR

T1 - A stratified semantics of general references embeddable in higher-order logic

AU - Ahmed, Amal J.

AU - Appel, Andrew Wilson

AU - Virga, Roberto

PY - 2002/1/1

Y1 - 2002/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0036052969&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0036052969&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:0036052969

SP - 75

EP - 86

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

SN - 1043-6871

ER -