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 | |
State | Published - Oct 22 2008 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)
Keywords
- Modal logic
- mechanical verification
- operational semantics
- separation logic