Extending Nunchaku to Dependent Type Theory
Simon Cruanes (Inria Nancy -- Grand Est), Jasmin Christian Blanchette, (Inria Nancy -- Grand Est, Max-Planck-Institut f\"ur Informatik)
TL;DR
This paper discusses extending the Nunchaku counterexample generator to support dependent types and type classes, aiming to improve its utility for proof assistants like Coq.
Contribution
It introduces initial ideas for adding partial dependent type support to Nunchaku, enhancing its applicability to systems based on dependent type theory.
Findings
Proposes extending Nunchaku with dependent type support
Aims to improve frontends for Coq and similar systems
Lays groundwork for future implementation
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.