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.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Robert Dockins, Andrew W. Appel, Aquinas Hobor
• Keywords: ENTCS 2008, Heterogeneous Multimodal Logic, Proof Assistant Coq, Separation Logic