Sciweavers

ENTCS
2008
136views more  ENTCS 2008»
14 years 15 days ago
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 heterogeneou...
Robert Dockins, Andrew W. Appel, Aquinas Hobor