Multimodal Separation Logic for Reasoning About Operational Semantics

Robert Dockins; Andrew W. Appel; Aquinas Hobor

doi:10.1016/j.entcs.2008.10.002

Multimodal Separation Logic for Reasoning About Operational Semantics

Robert Dockins, Andrew W. Appel, Aquinas Hobor

Research output: Contribution to journal › Article › peer-review

7 Scopus citations

Abstract

We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.

Original language	English (US)
Pages (from-to)	5-20
Number of pages	16
Journal	Electronic Notes in Theoretical Computer Science
Volume	218
Issue number	C
DOIs	https://doi.org/10.1016/j.entcs.2008.10.002
State	Published - Oct 22 2008

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Keywords

Modal logic
mechanical verification
operational semantics
separation logic

Access to Document

10.1016/j.entcs.2008.10.002

Cite this

@article{e07f7c88cbf84d24b87fc1f71be01a40,

title = "Multimodal Separation Logic for Reasoning About Operational Semantics",

abstract = "We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.",

keywords = "Modal logic, mechanical verification, operational semantics, separation logic",

author = "Robert Dockins and Appel, {Andrew W.} and Aquinas Hobor",

note = "Funding Information: Supported in part by National Science Foundation grants CCF-0540914 and CNS-0627650.",

year = "2008",

month = oct,

day = "22",

doi = "10.1016/j.entcs.2008.10.002",

language = "English (US)",

volume = "218",

pages = "5--20",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "C",

}

TY - JOUR

T1 - Multimodal Separation Logic for Reasoning About Operational Semantics

AU - Dockins, Robert

AU - Appel, Andrew W.

AU - Hobor, Aquinas

N1 - Funding Information: Supported in part by National Science Foundation grants CCF-0540914 and CNS-0627650.

PY - 2008/10/22

Y1 - 2008/10/22

N2 - We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.

AB - We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.

KW - Modal logic

KW - mechanical verification

KW - operational semantics

KW - separation logic

UR - http://www.scopus.com/inward/record.url?scp=54049146372&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=54049146372&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2008.10.002

DO - 10.1016/j.entcs.2008.10.002

M3 - Article

AN - SCOPUS:54049146372

SN - 1571-0661

VL - 218

SP - 5

EP - 20

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - C

ER -

Multimodal Separation Logic for Reasoning About Operational Semantics

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this