Compositional Proof Automation for Multi-level Abstractions


March 20, 2014


Reasoning about large systems requires reasoning about many different abstractions. For example, we can reason about state with separation logic, high-level specifications using sets and functions, and concrete implementations with bit-vectors and registers. In this talk, I discuss MirrorCore, a framework for building efficient, powerful procedures for reasoning about all of these abstractions and more. MirrorCore embraces and extends computational reflection with techniques for expressive, multi-level, extensible syntax in vanilla intensional type theory. Expressive syntax with binders and unification variables enables MirrorCore to reason about rich structures that include quantifiers. Further, extensible syntax coupled with a novel computational phrasing of open-world soundness enables composition of reflective procedures without falling back on proof-generating tactic languages. This composition enables more aggressive automation since side-conditions can be solved efficiently without breaking the flow of the computation.


Gregory Malecha

Gregory is currently a PhD candidate working on proof engineering and program verification with Greg Morrisett and Adam Chlipala. He is a recipient of a 2009 NSF Graduate Research Fellowship and a 2012 Facebook Fellowship. He started his PhD working on program verification in Hoare Type Theory using it to build the largest HTT programs at the time. As a Facebook Fellow, he began investigating scalable techniques for proof engineering and automation focusing on compositionality. His automation forms the core proof automation for the latest release of the Bedrock library for low-level program verification and is being adapted, and expanded, to work with several related projects.