Title: A stratified semantics of general references embeddable in higher-order logic
Abstract: 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.
Publication Year: 2003
Publication Date: 2003-06-25
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 45
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot