Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422038 | Electronic Notes in Theoretical Computer Science | 2008 | 16 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics