Logic in Computer Science (LICS 2002)

Paper: A Stratified Semantics of General References Embeddable in Higher-Order Logic (at LICS 2002)

Authors: Amal J. Ahmed Andrew W. Appel Roberto Virga

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.

BibTeX

  @InProceedings{AhmedAppelVirga-AStratifiedSemantic,
    author = 	 {Amal J. Ahmed and Andrew W. Appel and Roberto Virga},
    title = 	 {A Stratified Semantics of General References Embeddable in
    Higher-Order Logic},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }