Equations reloaded: high-level dependently-typed functional programming and proving in Coq
Equations reloaded: high-level dependently-typed functional programming and proving in Coq
复制标题
重新加载方程：Coq 中的高级依赖类型函数编程和证明
DOI：
10.1145/3341690
复制
发表时间：
2019
影响因子：
--
通讯作者：
Cyprien Mangin
中科院分区：
文献类型：
--
作者：
Matthieu Sozeau;Cyprien Mangin
方程是COQ证明助手的插件，它通过依赖的模式匹配和结构性或结构性的递归来定义程序，为定义程序提供了插件。此外，它还得出了有用的高级证明原则，用于展示有关它们的属性，从而从功能及其编译表格的实现细节中抽象出来。我们提出了一般的设计和实现，该设计和实现提供了可靠和表达的函数定义软件包，作为COQ内核的定义扩展。该系统的核心是基于对构造函数的无重点属性的原始处理，用于依赖平等的新简化器。
Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.