Compositional Proof Automation for Multi-level Abstractions

Опубликовано 21 июня 2016, 20:07

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.