一句话：提出 Coq 插件 Equations 的新设计与实现，支持依赖模式匹配和良基递归并自动导出高层证明原则。
本文关注在 Coq 中定义依赖类型程序时，依赖模式匹配与结构/良基递归的书写及相应证明原则的自动导出问题。作者提出 Equations 插件的新式通用设计与实现，将其作为 Coq 内核的定义式扩展，提供鲁棒且表达力强的函数定义包；系统核心是基于构造子 no-confusion 性质的新颖依赖等式化简器。该工作使用户能抽象掉函数实现及其编译形式，直接获得用于推理的高层证明原则，从而提升依赖类型函数式编程与证明的抽象层次。
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.
@article{paperbot609,
title = {Equations reloaded: high-level dependently-typed functional programming and proving in Coq},
author = {Matthieu Sozeau and Cyprien Mangin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341690}
}