Article ID Journal Published Year Pages File Type
422038 Electronic Notes in Theoretical Computer Science 2008 16 Pages PDF
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