← All papers
A metaprogramming framework for formal verification
cs.LO
Sep 1, 2017 · v1
TL;DR
Introduces Lean's tactic framework enabling user-defined proof automation in Lean itself.
Abstract
This paper describes the metaprogramming framework of the Lean theorem prover, which allows users to write custom proof automation, decision procedures, and tactics in the same language used for formal verification. The framework provides a monadic interface to the elaborator and type-checker, enabling reflective tactics and program transformations within a single unified environment.
Problem
Users of theorem provers need to write custom proof automation, decision procedures, and tactics, but doing so in a separate metalanguage creates friction and limits expressiveness.
Approach
The paper describes the metaprogramming framework of the Lean theorem prover, which provides a monadic interface to the elaborator and type-checker. Users write custom tactics and program transformations in the same language used for formal verification, enabling reflective tactics within a single unified environment.
Results
The framework enables users to implement custom proof automation and decision procedures directly in Lean, supporting reflective tactics and program transformations without leaving the verification language.