Sciweavers

Share
ENTCS
2008

Multimodal Separation Logic for Reasoning About Operational Semantics

11 years 1 months ago
Multimodal Separation Logic for Reasoning About Operational Semantics
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.
Robert Dockins, Andrew W. Appel, Aquinas Hobor
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Robert Dockins, Andrew W. Appel, Aquinas Hobor
Comments (0)
books