一句话：在 Lean 中实现面向形式验证的元编程框架，通过反射对象级表达式支持高效编写 tactic 与自动化。
交互式定理证明器通常需要用户编写策略与自动化，但直接扩展证明器内部结构往往困难且性能受限。本文介绍 Lean 中实际采用的元编程框架：它在依赖类型理论的对象语言之上提供访问 Lean 内部数据结构与过程的 API，并支持将对象层表达式反射到元语言，从而让用户以统一方式编写元程序。作者用性能证据表明该实现高效，并展示该框架不仅能便捷地编写小规模交互式 tactic，还足以支撑更实质的自动化开发。
We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.
@article{EbnerURAM17,
title = {A metaprogramming framework for formal verification},
author = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110278}
}