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

Amal J. Ahmed; Andrew W. Appel; Roberto Virga

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

Amal J. Ahmed, Andrew W. Appel, Roberto Virga

Research output: Contribution to journal › Conference article › peer-review

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 - 2002
Event	17th Annual IEEE Symposium on Logic in Computer Science - Copenhagen, Denmark Duration: Jul 22 2002 → Jul 25 2002

All Science Journal Classification (ASJC) codes

Software
General Mathematics

Cite this

@article{0533b6a3e0144cefa99d89a37267df40,

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.",

author = "Ahmed, {Amal J.} and Appel, {Andrew W.} and Roberto Virga",

year = "2002",

language = "English (US)",

pages = "75--86",

journal = "Proceedings - Symposium on Logic in Computer Science",

issn = "1043-6871",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

note = "17th Annual IEEE Symposium on Logic in Computer Science ; Conference date: 22-07-2002 Through 25-07-2002",

}

TY - JOUR

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

AU - Ahmed, Amal J.

AU - Appel, Andrew W.

AU - Virga, Roberto

PY - 2002

Y1 - 2002

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

SN - 1043-6871

SP - 75

EP - 86

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

T2 - 17th Annual IEEE Symposium on Logic in Computer Science

Y2 - 22 July 2002 through 25 July 2002

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this