Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Compositional Proof Automation for Multi-level Abstractions

Speaker  Gregory Malecha

Affiliation  Harvard School of Engineering and Applied Sciences

Host  Nick Benton

Duration  00:55:38

Date recorded  19 March 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.

©2014 Microsoft Corporation. All rights reserved.
> Compositional Proof Automation for Multi-level Abstractions