6 citations · 6 across the 1 of their papers we have counts for
3 papers
Language and Proofs for Higher-Order SMT (Work in Progress)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes +2
Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo…
Extending Nunchaku to Dependent Type Theory
Simon Cruanes, Jasmin Christian Blanchette
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 Nitp…
Proceedings First International Workshop on Hammers for Type Theories
Jasmin Christian Blanchette, Cezary Kaliszyk
This volume of EPTCS contains the proceedings of the First Workshop on Hammers for Type Theories (HaTT 2016), held on 1 July 2016 as part of the International Joint Conference on A…