### 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 language | English (US) |
---|---|

Pages (from-to) | 75-86 |

Number of pages | 12 |

Journal | Proceedings - Symposium on Logic in Computer Science |

State | Published - 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

Ahmed, A. J., Appel, A. W., & Virga, R. (2002). A stratified semantics of general references embeddable in higher-order logic.

*Proceedings - Symposium on Logic in Computer Science*, 75-86.