The Lean 4 Theorem Prover and Programming Language
The Lean 4 Theorem Prover and Programming Language
复制标题
Lean 4 定理证明器和编程语言
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Sebastian Ullrich
中科院分区：
文献类型：
--
作者：
L. D. Moura;Sebastian Ullrich
精益4是精益交互式定理证明器（ITP）的重新实现。它解决了以前版本的许多缺点，并包含许多新功能。Lean 4是完全可扩展的：用户可以修改和扩展解析器，阐述器，策略，决策过程，漂亮的打印机和代码生成器。新系统具有为ITP定制的卫生宏观系统。它包含了一个新的typeclass决议程序的基础上表的决议，解决日益增长的用户群报告的重大性能问题。Lean 4也是一种高效的函数式编程语言，它基于一种名为functional but in-place的新型编程范式。高效的代码生成对于Lean用户来说至关重要，因为许多人在Lean中编写自定义的自动化验证过程。
Lean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom proof automation procedures in Lean itself.
精益计划
影响因子：
0.5
作者：
Buzzard K
通讯作者：
Buzzard K