Speaker Gregory Malecha
Affiliation Harvard School of Engineering and Applied Sciences
Host Nick Benton
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.