将 Nunchaku 扩展至依值类型理论
计算机科学中的逻辑
2016-06-21 v1
摘要
Nunchaku 是一种新型高阶反例生成器，基于从多态高阶逻辑到一阶逻辑的一系列转换。与其前身——用于 Isabelle 的 Nitpick——不同，它被设计为一个独立工具，并为各种证明助手提供前端。在这篇短文中，我们介绍了一些将 Nunchaku 扩展以部分支持依值类型与类型类的想法，旨在使 Coq 及其他基于依值类型理论的系统的前端更加实用。
引用
@article{arxiv.1606.05945,
title = {Extending Nunchaku to Dependent Type Theory},
author = {Simon Cruanes and Jasmin Christian Blanchette},
journal= {arXiv preprint arXiv:1606.05945},
year = {2016}
}
备注
In Proceedings HaTT 2016, arXiv:1606.05427