Multimodal Separation Logic for Reasoning About Operational Semantics

Robert Dockins, Andrew W. Appel, Aquinas Hobor

Research output: Contribution to journalArticlepeer-review

7 Scopus citations


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 languageEnglish (US)
Pages (from-to)5-20
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Issue numberC
StatePublished - Oct 22 2008

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Modal logic
  • mechanical verification
  • operational semantics
  • separation logic


Dive into the research topics of 'Multimodal Separation Logic for Reasoning About Operational Semantics'. Together they form a unique fingerprint.

Cite this