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

Amal J. Ahmed, Andrew Wilson Appel, Roberto Virga

Research output: Contribution to journalConference article

26 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)75-86
Number of pages12
JournalProceedings - Symposium on Logic in Computer Science
StatePublished - Jan 1 2002

All Science Journal Classification (ASJC) codes

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'A stratified semantics of general references embeddable in higher-order logic'. Together they form a unique fingerprint.

  • Cite this