Jasmin Blanchette

According to our database, Jasmin Blanchette authored at least 98 papers between 2006 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Complete and Efficient Higher-Order Reasoning via Lambda-Superposition.

Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann

ACM SIGLOG News, October, 2023

Unifying Splitting.

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret

J. Autom. Reason., June, 2023

Superposition for Higher-Order Logic.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic

J. Autom. Reason., March, 2023

SAT-Inspired Eliminations for Superposition.

Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule

ACM Trans. Comput. Log., January, 2023

SAT-Inspired Higher-Order Eliminations.

Jasmin Blanchette, Petar Vukmirovic

Log. Methods Comput. Sci., 2023

Closure Properties of Unrestricted Grammars - Formally Verified.

Martin Dvorak, Jasmin Blanchette

CoRR, 2023

Mechanical Mathematicians.

Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann

Commun. ACM, 2023

Given Clause Loops.

Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret

Arch. Formal Proofs, 2023

Extending a High-Performance Prover to Higher-Order Logic.

Petar Vukmirovic, Jasmin Blanchette, Stephan Schulz

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Closure Properties of General Grammars - Formally Verified.

Martin Dvorak, Jasmin Blanchette

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Recurrence-Driven Summations in Automated Deduction.

Visa Nummelin, Jasmin Blanchette, Sander R. Dahmen

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Verified Given Clause Procedures.

Jasmin Blanchette, Qi Qiu, Sophie Tourret

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Extending a brainiac prover to lambda-free higher-order logic.

Petar Vukmirovic, Jasmin Blanchette, Simon Cruanes, Stephan Schulz

Int. J. Softw. Tools Technol. Transf., 2022

A Comprehensive Framework for Saturation Theorem Proving.

Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette

J. Autom. Reason., 2022

Making Higher-Order Superposition Work.

Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret

J. Autom. Reason., 2022

Seventeen Provers Under the Hammer.

Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Superposition for Lambda-Free Higher-Order Logic.

Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann

Log. Methods Comput. Sci., 2021

Message from the New Editor-in-Chief.

Jasmin Blanchette

J. Autom. Reason., 2021

Superposition with Lambdas.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann

J. Autom. Reason., 2021

FMM Preface.

Jasmin Blanchette, Adam Naumowicz

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

A modular Isabelle framework for verifying saturation provers.

Sophie Tourret, Jasmin Blanchette

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

A Unifying Splitting Framework.

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret

Proceedings of the Automated Deduction - CADE 28, 2021

Superposition for Full Higher-order Logic.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann

J. Autom. Reason., 2020

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

J. Autom. Reason., 2020

Extensions to the Comprehensive Framework for Saturation Theorem Proving.

Jasmin Blanchette, Sophie Tourret

Arch. Formal Proofs, 2020

2019

Introduction to the STAF 2015 special section.

Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer

Softw. Syst. Model., 2019

Bindings as bounded natural functors.

Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel

Proc. ACM Program. Lang., 2019

Selected Extended Papers of ITP 2016: Preface.

Jasmin Christian Blanchette, Stephan Merz

J. Autom. Reason., 2019

A Formal Proof of the Expressiveness of Deep Learning.

Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow

J. Autom. Reason., 2019

A verified prover based on ordered resolution.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk).

Jasmin Christian Blanchette

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

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

Introduction to Milestones in Interactive Theorem Proving.

Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting

J. Autom. Reason., 2018

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Arch. Formal Proofs, 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 SAT solver with watched literals using imperative HOL.

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Superposition with Datatypes and Codatatypes.

Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

A Decision Procedure for (Co)datatypes in SMT Solvers.

Andrew Reynolds, Jasmin Christian Blanchette

J. Autom. Reason., 2017

Soundness and Completeness Proofs by Coinductive Methods.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

J. Autom. Reason., 2017

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371).

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli

Dagstuhl Reports, 2017

Language and Proofs for Higher-Order SMT (Work in Progress).

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine

Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Operations on Bounded Natural Functors.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2017

Abstract Soundness.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2017

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Foundational nonuniform (Co)datatypes for higher-order logic.

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 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, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

A Lambda-Free Higher-Order Recursive Path Order.

Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Proceedings of the Foundations of Software Science and Computation Structures, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

Proceedings of the Programming Languages and Systems, 2017

Towards Strong Higher-Order Automation for Fast Interactive Verification.

Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann

Proceedings of the ARCADE 2017, 2017

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms.

Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Proceedings of the Automated Deduction - CADE 26, 2017

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Hammering towards QED.

Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban

J. Formaliz. 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

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

Extending Nunchaku to Dependent Type Theory.

Simon Cruanes, Jasmin Christian Blanchette

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

Encoding Monomorphic and Polymorphic Types.

Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone

Log. Methods Comput. Sci., 2016

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms.

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 Knuth-Bendix Orders for Lambda-Free Higher-Order Terms.

Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Arch. Formal Proofs, 2016

Model Finding for Recursive Functions in SMT.

Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.

Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

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

Foundational Extensible Corecursion.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

CoRR, 2015

Mining the Archive of Formal Proofs.

Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Foundational extensible corecursion: a proof assistant perspective.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Witnessing (Co)datatypes.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Programming Languages and Systems, 2015

2014

Abstract Completeness.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.

Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Cardinals in Isabelle/HOL.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Experience report: the next 1100 Haskell programmers.

Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel

Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

My Life with an Automatic Theorem Prover.

Jasmin Christian Blanchette

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

Unified Classical Logic Completeness - A Coinductive Pearl.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions.

Jasmin Christian Blanchette

Softw. Qual. J., 2013

Extending Sledgehammer with SMT Solvers.

Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson

J. Autom. Reason., 2013

LEO-II and Satallax on the Sledgehammer test bench.

Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson

J. Appl. Log., 2013

Sound and Complete Sort Encodings for First-Order Logic.

Jasmin Christian Blanchette, Andrei Popescu

Arch. Formal Proofs, 2013

MaSh: Machine Learning for Sledgehammer.

Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Mechanizing the Metatheory of Sledgehammer.

Jasmin Christian Blanchette, Andrei Popescu

Proceedings of the Frontiers of Combining Systems, 2013

Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs.

Steffen Juilf Smolka, Jasmin Christian Blanchette

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.

Jasmin Christian Blanchette, Andrei Paskevich

Proceedings of the Automated Deduction - CADE-24, 2013

Redirecting Proofs by Contradiction.

Jasmin Christian Blanchette

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

Automatic proofs and refutations for higher-order logic.

Jasmin Christian Blanchette

PhD thesis, 2012

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.

Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.

Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Monotonicity Inference for Higher-Order Formulas.

Jasmin Christian Blanchette, Alexander Krauss

J. Autom. Reason., 2011

Nitpicking C++ concurrency.

Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Automatic Proof and Disproof in Isabelle/HOL.

Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.

Lawrence C. Paulson, Jasmin Christian Blanchette

Proceedings of the 8th International Workshop on the Implementation of Logics, 2010

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models.

Jasmin Christian Blanchette, Koen Claessen

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod.

Jasmin Christian Blanchette

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.

Jasmin Christian Blanchette, Tobias Nipkow

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.

Jasmin Christian Blanchette

J. Autom. Reason., 2009

2008

Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol.

Einar Broch Johnsen, Jasmin Christian Blanchette, Marcel Kyas, Olaf Owe

Proceedings of the 2nd International Workshop on Harnessing Theories for Tool Support in Software, 2008

The Textbook Proof of Huffman's Algorithm.

Jasmin Christian Blanchette

Arch. Formal Proofs, 2008

C++ GUI Programming with Qt 4, 2nd Edition.

Jasmin Blanchette, Mark Summerfield

Pearson Education, ISBN: 978-0-13-235416-5, 2008

2007

An Open System Operational Semantics for an Object-Oriented and Component-Based Language.

Jasmin Christian Blanchette, Olaf Owe

Proceedings of the 4th International Workshop on Formal Aspects of Component Software, 2007

2006

C++ GUI programming with Qt 4.

Jasmin Christian Blanchette, Mark Summerfield

Prentice Hall, ISBN: 0131872494, 2006