| 2019 | CPP | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). | Jasmin Christian Blanchette |
| 2019 | CPP | A verified prover based on ordered resolution. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
| 2019 | TACAS | Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. | Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz |
| 2018 | CADE | Superposition for Lambda-Free Higher-Order Logic. | Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann |
| 2018 | CADE | Superposition with Datatypes and Codatatypes. | Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard |
| 2018 | CADE | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann |
| 2018 | CPP | A verified SAT solver with watched literals using imperative HOL. | Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
| 2017 | CADE | Scalable Fine-Grained Proofs for Formula Processing. | Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine |
| 2017 | CADE | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2017 | CADE | Towards Strong Higher-Order Automation for Fast Interactive Verification. | Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann |
| 2017 | ESOP | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. | Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | FOSSACS | A Lambda-Free Higher-Order Recursive Path Order. | Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2017 | IJCAI | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2017 | ITP | A Formal Proof of the Expressiveness of Deep Learning. | Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow |
| 2017 | LICS | Foundational nonuniform (Co)datatypes for higher-order logic. | Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel |
| 2016 | CADE | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2016 | CADE | Model Finding for Recursive Functions in SMT. | Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
| 2016 | IJCAI | A Decision Procedure for (Co)datatypes in SMT Solvers. | Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | CADE | A Decision Procedure for (Co)datatypes in SMT Solvers. | Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | ESOP | Witnessing (Co)datatypes. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2015 | ICFP | Foundational extensible corecursion: a proof assistant perspective. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | CADE | Unified Classical Logic Completeness - A Coinductive Pearl. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | CADE | My Life with an Automatic Theorem Prover. | Jasmin Christian Blanchette |
| 2014 | HASKELL | Experience report: the next 1100 Haskell programmers. | Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel |
| 2014 | ITP | Cardinals in Isabelle/HOL. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2013 | CADE | Redirecting Proofs by Contradiction. | Jasmin Christian Blanchette |
| 2013 | CADE | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. | Jasmin Christian Blanchette, Andrei Paskevich |
| 2013 | CADE | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. | Steffen Juilf Smolka, Jasmin Christian Blanchette |
| 2013 | ITP | MaSh: Machine Learning for Sledgehammer. | Daniel Khlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
| 2013 | TACAS | Encoding Monomorphic and Polymorphic Types. | Jasmin Christian Blanchette, Sascha Bhme, Andrei Popescu, Nicholas Smallbone |
| 2012 | ITP | More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. | Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach |
| 2012 | LICS | Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. | Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette |
| 2011 | CADE | Extending Sledgehammer with SMT Solvers. | Jasmin Christian Blanchette, Sascha Bhme, Lawrence C. Paulson |
| 2011 | PPDP | Nitpicking C++ concurrency. | Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar |
| 2010 | CADE | Monotonicity Inference for Higher-Order Formulas. | Jasmin Christian Blanchette, Alexander Krauss |
| 2010 | ITP | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. | Jasmin Christian Blanchette, Tobias Nipkow |
| 2010 | LPAR | Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod. | Jasmin Christian Blanchette |
| 2010 | LPAR | Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. | Jasmin Christian Blanchette, Koen Claessen |
| 2010 | LPAR | Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. | Lawrence C. Paulson, Jasmin Christian Blanchette |
| 2010 | TAP | Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions. | Jasmin Christian Blanchette |