A metaprogramming framework for formal verification

  • ,
  • Sebastian Ullrich ,
  • Jared Roesch ,
  • Jeremy Avigad ,
  • Leonardo de Moura

ICFP 2017 |

PDF

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.

论文与出版物下载

Lean 4

4 1 月, 2021

Lean 4 programming language and theorem prover Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming. Learn more about Lean 4 >