Jasmin Christian Blanchette

ORCID

Publication Activity (10 Years)

Years Active: 2008-2023
Publications (10 Years): 43

Top Venues

Technical University Munich (PHD)

Education History

Technical University Munich

PHD

Publications

Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret
Given Clause Loops. Arch. Formal Proofs 2023 (2023)
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64 (3) (2020)
Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. TACAS (1) (2019)
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
A Formal Proof of the Expressiveness of Deep Learning. J. Autom. Reason. 63 (2) (2019)
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3 (POPL) (2019)
Jasmin Christian Blanchette
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). CPP (2019)
Jasmin Christian Blanchette, Stephan Merz
Selected Extended Papers of ITP 2016: Preface. J. Autom. Reason. 62 (2) (2019)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
A verified prover based on ordered resolution. CPP (2019)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
Superposition with Datatypes and Codatatypes. IJCAR (2018)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR (2018)
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann
Superposition for Lambda-Free Higher-Order Logic. IJCAR (2018)
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61 (1-4) (2018)
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
A verified SAT solver with watched literals using imperative HOL. CPP (2018)
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61 (1-4) (2018)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE (2017)
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
A Lambda-Free Higher-Order Recursive Path Order. FoSSaCS (2017)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Soundness. Arch. Formal Proofs 2017 (2017)
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP (2017)
Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7 (9) (2017)
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE (2017)
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
A Formal Proof of the Expressiveness of Deep Learning. ITP (2017)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58 (3) (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58 (1) (2017)
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
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS (2017)
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. CADE (2017)
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD (2017)
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
Foundational nonuniform (Co)datatypes for higher-order logic. LICS (2017)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI (2016)
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016)
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. 56 (2) (2016)
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. 57 (3) (2016)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016)
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016)
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR (2016)
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
Model Finding for Recursive Functions in SMT. IJCAR (2016)
Simon Cruanes, Jasmin Christian Blanchette
Extending Nunchaku to Dependent Type Theory. HaTT@IJCAR (2016)
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
Hammering towards QED. J. Formaliz. Reason. 9 (1) (2016)
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12 (4) (2016)
Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow
Mining the Archive of Formal Proofs. CICM (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational extensible corecursion: a proof assistant perspective. ICFP (2015)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion. CoRR (2015)
Nikolaj Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5 (9) (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Witnessing (Co)datatypes. ESOP (2015)
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Cardinals in Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Completeness. Arch. Formal Proofs 2014 (2014)
Jasmin Christian Blanchette
My Life with an Automatic Theorem Prover. Vampire Workshop (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR (2014)
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
Experience report: the next 1100 Haskell programmers. Haskell (2014)
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban
MaSh: Machine Learning for Sledgehammer. ITP (2013)
Jasmin Christian Blanchette
Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. Softw. Qual. J. 21 (1) (2013)
Jasmin Christian Blanchette, Andrei Popescu
Mechanizing the Metatheory of Sledgehammer. FroCos (2013)
Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson
LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11 (1) (2013)
Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51 (1) (2013)
Jasmin Christian Blanchette, Andrei Paskevich
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. CADE (2013)
Jasmin Christian Blanchette
Redirecting Proofs by Contradiction. PxTP@CADE (2013)
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types. TACAS (2013)
Steffen Juilf Smolka, Jasmin Christian Blanchette
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. PxTP@CADE (2013)
Jasmin Christian Blanchette, Andrei Popescu
Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs 2013 (2013)
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP (2012)
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS (2012)
Jasmin Christian Blanchette, Alexander Krauss
Monotonicity Inference for Higher-Order Formulas. J. Autom. Reason. 47 (4) (2011)
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar
Nitpicking C++ concurrency. PPDP (2011)
Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson
Extending Sledgehammer with SMT Solvers. CADE (2011)
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
Automatic Proof and Disproof in Isabelle/HOL. FroCoS (2011)
Jasmin Christian Blanchette
Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions. TAP@TOOLS (2010)
Lawrence C. Paulson, Jasmin Christian Blanchette
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR (2010)
Jasmin Christian Blanchette
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod. LPAR short papers(Yogyakarta) (2010)
Jasmin Christian Blanchette, Alexander Krauss
Monotonicity Inference for Higher-Order Formulas. IJCAR (2010)
Jasmin Christian Blanchette, Tobias Nipkow
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP (2010)
Jasmin Christian Blanchette, Koen Claessen
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. LPAR (Yogyakarta) (2010)
Jasmin Christian Blanchette
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. J. Autom. Reason. 43 (1) (2009)
Einar Broch Johnsen, Jasmin Christian Blanchette, Marcel Kyas, Olaf Owe
Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol. Electron. Notes Theor. Comput. Sci. 243 (2009)
Jasmin Christian Blanchette
The Textbook Proof of Huffman's Algorithm. Arch. Formal Proofs 2008 (2008)
Jasmin Christian Blanchette, Olaf Owe
An Open System Operational Semantics for an Object-Oriented and Component-Based Language. Electron. Notes Theor. Comput. Sci. 215 (2008)

Jasmin Christian Blanchette.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Jasmin Christian Blanchette