将双节棍扩展到依赖类型论
Extending Nunchaku to Dependent Type Theory
摘要：
双节棍是一种新的高阶反例生成器，它基于一系列从多态高阶逻辑到一阶逻辑的变换。与其前身Nitpick for Isabelle不同，它被设计为一个独立的工具，具有各种证明助手的前端。在这篇简短的论文中，我们提出了一些想法来扩展Nunchaku，部分支持依赖类型和类型类，使Coq和其他基于依赖类型论的系统的前端更有用。
英文摘要：
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
