Extending Nunchaku to Dependent Type Theory
Logic in Computer Science
2016-06-21 v1
Abstract
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.
Cite
@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}
}
Comments
In Proceedings HaTT 2016, arXiv:1606.05427