C++ GUI programming with Qt 4. - Jasmin Christian Blanchette; Mark Summerfield (Prentice Hall, 2006)

An Open System Operational Semantics for an Object-Oriented and Component-Based Language. - Jasmin Christian Blanchette; Olaf Owe (FACS, 2007)

C++ GUI Programming with Qt 4, 2nd Edition. - Jasmin Blanchette; Mark Summerfield (Pearson Education, 2008)

The Textbook Proof of Huffman's Algorithm. - Jasmin Christian Blanchette (Arch. Formal Proofs, 2008)

Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol. - Einar Broch Johnsen; Jasmin Christian Blanchette; Marcel Kyas; Olaf Owe (TTSS, 2008)

Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. - Jasmin Christian Blanchette (J. Autom. Reason., 2009)

Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. - Jasmin Christian Blanchette; Tobias Nipkow (ITP, 2010)

Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod. - Jasmin Christian Blanchette (LPAR short papers(Yogyakarta), 2010)

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. - Jasmin Christian Blanchette; Koen Claessen (LPAR (Yogyakarta), 2010)

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. - Lawrence C. Paulson; Jasmin Christian Blanchette (IWIL@LPAR, 2010)

Automatic Proof and Disproof in Isabelle/HOL. - Jasmin Christian Blanchette; Lukas Bulwahn; Tobias Nipkow (FroCoS, 2011)

Nitpicking C++ concurrency. - Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar (PPDP, 2011)

Monotonicity Inference for Higher-Order Formulas. - Jasmin Christian Blanchette; Alexander Krauss 001 (J. Autom. Reason., 2011)

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. - Jasmin Christian Blanchette; Andrei Popescu 001; Daniel Wand; Christoph Weidenbach (ITP, 2012)

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. - Dmitriy Traytel; Andrei Popescu 001; Jasmin Christian Blanchette (LICS, 2012)

Automatic proofs and refutations for higher-order logic. - Jasmin Christian Blanchette (2012)

Redirecting Proofs by Contradiction. - Jasmin Christian Blanchette (PxTP@CADE, 2013)

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. - Jasmin Christian Blanchette; Andrei Paskevich (CADE, 2013)

Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. - Steffen Juilf Smolka; Jasmin Christian Blanchette (PxTP@CADE, 2013)

Mechanizing the Metatheory of Sledgehammer. - Jasmin Christian Blanchette; Andrei Popescu 001 (FroCos, 2013)

MaSh: Machine Learning for Sledgehammer. - Daniel Kühlwein; Jasmin Christian Blanchette; Cezary Kaliszyk; Josef Urban (ITP, 2013)

Sound and Complete Sort Encodings for First-Order Logic. - Jasmin Christian Blanchette; Andrei Popescu 001 (Arch. Formal Proofs, 2013)

LEO-II and Satallax on the Sledgehammer test bench. - Nik Sultana; Jasmin Christian Blanchette; Lawrence C. Paulson (J. Appl. Log., 2013)

Extending Sledgehammer with SMT Solvers. - Jasmin Christian Blanchette; Sascha Böhme; Lawrence C. Paulson (J. Autom. Reason., 2013)

Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. - Jasmin Christian Blanchette (Softw. Qual. J., 2013)

Unified Classical Logic Completeness - A Coinductive Pearl. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (IJCAR, 2014)

My Life with an Automatic Theorem Prover. - Jasmin Christian Blanchette (Vampire Workshop, 2014)

Experience report: the next 1100 Haskell programmers. - Jasmin Christian Blanchette; Lars Hupel; Tobias Nipkow; Lars Noschinski; Dmitriy Traytel (Haskell, 2014)

Cardinals in Isabelle/HOL. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Truly Modular (Co)datatypes for Isabelle/HOL. - Jasmin Christian Blanchette; Johannes Hölzl; Andreas Lochbihler; Lorenz Panny; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Abstract Completeness. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2014)

Witnessing (Co)datatypes. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2015)

Foundational extensible corecursion: a proof assistant perspective. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ICFP, 2015)

Mining the Archive of Formal Proofs. - Jasmin Christian Blanchette; Max W. Haslbeck; Daniel Matichuk; Tobias Nipkow (CICM, 2015)

Foundational Extensible Corecursion. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (CoRR, 2015)

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). - Nikolaj S. Bjørner; Jasmin Christian Blanchette; Viorica Sofronie-Stokkermans; Christoph Weidenbach (Dagstuhl Reports, 2015)

Model Finding for Recursive Functions in SMT. - Andrew Reynolds 001; Jasmin Christian Blanchette; Simon Cruanes; Cesare Tinelli (IJCAR, 2016)

Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. - Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (Arch. Formal Proofs, 2016)

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. - Jasmin Christian Blanchette; Mathias Fleury; Dmitriy Traytel (Arch. Formal Proofs, 2016)

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. - Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (Arch. Formal Proofs, 2016)

Encoding Monomorphic and Polymorphic Types. - Jasmin Christian Blanchette; Sascha Böhme; Andrei Popescu 001; Nicholas Smallbone (Log. Methods Comput. Sci., 2016)

Extending Nunchaku to Dependent Type Theory. - Simon Cruanes; Jasmin Christian Blanchette (HaTT@IJCAR, 2016)

Semi-intelligible Isar Proofs from Machine-Generated Proofs. - Jasmin Christian Blanchette; Sascha Böhme; Mathias Fleury; Steffen Juilf Smolka; Albert Steckermeier (J. Autom. Reason., 2016)

A Learning-Based Fact Selector for Isabelle/HOL. - Jasmin Christian Blanchette; David Greenaway; Cezary Kaliszyk; Daniel Kühlwein; Josef Urban (J. Autom. Reason., 2016)

Hammering towards QED. - Jasmin Christian Blanchette; Cezary Kaliszyk; Lawrence C. Paulson; Josef Urban (J. Formaliz. Reason., 2016)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Pascal Fontaine (CADE, 2017)

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. - Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (CADE, 2017)

Towards Strong Higher-Order Automation for Fast Interactive Verification. - Jasmin Christian Blanchette; Pascal Fontaine; Stephan Schulz 001; Uwe Waldmann (ARCADE@CADE, 2017)

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. - Jasmin Christian Blanchette; Aymeric Bouzy; Andreas Lochbihler; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2017)

A Lambda-Free Higher-Order Recursive Path Order. - Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (FoSSaCS, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Christoph Weidenbach (IJCAI, 2017)

Foundational nonuniform (Co)datatypes for higher-order logic. - Jasmin Christian Blanchette; Fabian Meier; Andrei Popescu 001; Dmitriy Traytel (LICS, 2017)

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. - Jasmin Christian Blanchette; Mathias Fleury; Dmitriy Traytel (FSCD, 2017)

Abstract Soundness. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2017)

Operations on Bounded Natural Functors. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2017)

Language and Proofs for Higher-Order SMT (Work in Progress). - Haniel Barbosa; Jasmin Christian Blanchette; Simon Cruanes; Daniel El Ouraoui; Pascal Fontaine (PxTP, 2017)

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). - Jasmin Christian Blanchette; Carsten Fuhs; Viorica Sofronie-Stokkermans; Cesare Tinelli (Dagstuhl Reports, 2017)

Soundness and Completeness Proofs by Coinductive Methods. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (J. Autom. Reason., 2017)

A Decision Procedure for (Co)datatypes in SMT Solvers. - Andrew Reynolds 001; Jasmin Christian Blanchette (J. Autom. Reason., 2017)

Superposition with Datatypes and Codatatypes. - Jasmin Christian Blanchette; Nicolas Peltier; Simon Robillard (IJCAR, 2018)

A verified SAT solver with watched literals using imperative HOL. - Mathias Fleury; Jasmin Christian Blanchette; Peter Lammich (CPP, 2018)

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. - Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel; Uwe Waldmann (Arch. Formal Proofs, 2018)

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. - Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel (Arch. Formal Proofs, 2018)

Introduction to Milestones in Interactive Theorem Proving. - Jeremy Avigad; Jasmin Christian Blanchette; Gerwin Klein; Lawrence C. Paulson; Andrei Popescu 001; Gregor Snelting (J. Autom. Reason., 2018)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Peter Lammich; Christoph Weidenbach (J. Autom. Reason., 2018)

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). - Jasmin Christian Blanchette (CPP, 2019)

A verified prover based on ordered resolution. - Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel (CPP, 2019)

A Formal Proof of the Expressiveness of Deep Learning. - Alexander Bentkamp; Jasmin Christian Blanchette; Dietrich Klakow (J. Autom. Reason., 2019)

Selected Extended Papers of ITP 2016: Preface. - Jasmin Christian Blanchette; Stephan Merz (J. Autom. Reason., 2019)

Bindings as bounded natural functors. - Jasmin Christian Blanchette; Lorenzo Gheri; Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2019)

Introduction to the STAF 2015 special section. - Jasmin Blanchette; Francis Bordeleau; Alfonso Pierantonio; Nikolai Kosmatov; Gabriele Taentzer; Manuel Wimmer (Softw. Syst. Model., 2019)

Extensions to the Comprehensive Framework for Saturation Theorem Proving. - Jasmin Blanchette; Sophie Tourret (Arch. Formal Proofs, 2020)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Mathias Fleury; Pascal Fontaine (J. Autom. Reason., 2020)

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. - Anders Schlichtkrull; Jasmin Blanchette; Dmitriy Traytel; Uwe Waldmann (J. Autom. Reason., 2020)

Superposition for Full Higher-order Logic. - Alexander Bentkamp; Jasmin Blanchette; Sophie Tourret; Petar Vukmirovic (CADE, 2021)

A Unifying Splitting Framework. - Gabriel Ebner; Jasmin Blanchette; Sophie Tourret (CADE, 2021)

A modular Isabelle framework for verifying saturation provers. - Sophie Tourret; Jasmin Blanchette (CPP, 2021)

FMM Preface. - Jasmin Blanchette; Adam Naumowicz (CICM Workshops, 2021)

Superposition with Lambdas. - Alexander Bentkamp; Jasmin Blanchette; Sophie Tourret; Petar Vukmirovic; Uwe Waldmann (J. Autom. Reason., 2021)

Message from the New Editor-in-Chief. - Jasmin Blanchette (J. Autom. Reason., 2021)

Superposition for Lambda-Free Higher-Order Logic. - Alexander Bentkamp; Jasmin Blanchette; Simon Cruanes; Uwe Waldmann (Log. Methods Comput. Sci., 2021)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (Zenodo, 2021)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (Zenodo, 2021)

Seventeen Provers Under the Hammer. - Martin Desharnais; Petar Vukmirovic; Jasmin Blanchette; Makarius Wenzel (ITP, 2022)

Making Higher-Order Superposition Work. - Petar Vukmirovic; Alexander Bentkamp; Jasmin Blanchette; Simon Cruanes; Visa Nummelin; Sophie Tourret (J. Autom. Reason., 2022)

A Comprehensive Framework for Saturation Theorem Proving. - Uwe Waldmann; Sophie Tourret; Simon Robillard; Jasmin Blanchette (J. Autom. Reason., 2022)

Extending a brainiac prover to lambda-free higher-order logic. - Petar Vukmirovic; Jasmin Blanchette; Simon Cruanes; Stephan Schulz 001 (Int. J. Softw. Tools Technol. Transf., 2022)

Verified Given Clause Procedures. - Jasmin Blanchette; Qi Qiu; Sophie Tourret (CADE, 2023)

Recurrence-Driven Summations in Automated Deduction. - Visa Nummelin; Jasmin Blanchette; Sander R. Dahmen (FroCoS, 2023)

Closure Properties of General Grammars - Formally Verified. - Martin Dvorak; Jasmin Blanchette (ITP, 2023)

Extending a High-Performance Prover to Higher-Order Logic. - Petar Vukmirovic; Jasmin Blanchette; Stephan Schulz 001 (TACAS (2), 2023)

Given Clause Loops. - Jasmin Christian Blanchette; Qi Qiu; Sophie Tourret (Arch. Formal Proofs, 2023)

Mechanical Mathematicians. - Alexander Bentkamp; Jasmin Blanchette; Visa Nummelin; Sophie Tourret; Petar Vukmirovic; Uwe Waldmann (Commun. ACM, 2023)

Closure Properties of Unrestricted Grammars - Formally Verified. - Martin Dvorak; Jasmin Blanchette (CoRR, 2023)

SAT-Inspired Higher-Order Eliminations. - Jasmin Blanchette; Petar Vukmirovic (Log. Methods Comput. Sci., 2023)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (ACM Trans. Comput. Log., 2023)

Superposition for Higher-Order Logic. - Alexander Bentkamp; Jasmin Blanchette; Sophie Tourret; Petar Vukmirovic (J. Autom. Reason., 2023)

Unifying Splitting. - Gabriel Ebner; Jasmin Blanchette; Sophie Tourret (J. Autom. Reason., 2023)

Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. - Alexander Bentkamp; Jasmin Blanchette; Visa Nummelin; Sophie Tourret; Uwe Waldmann (ACM SIGLOG News, 2023)

A Modular Formalization of Superposition in Isabelle/HOL. - Martin Desharnais; Balázs Tóth; Uwe Waldmann; Jasmin Blanchette; Sophie Tourret (ITP, 2024)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. - Lukas Bartl; Jasmin Blanchette; Tobias Nipkow (CADE, 2025)

Augmenting Model-Based Instantiation with Fast Enumeration. - Lydia Kondylidou; Andrew Reynolds 001; Jasmin Blanchette (TACAS (1), 2025)