Jasmin Christian Blanchette

87 papers A* 4A 16B 12C 3Journal 31Unranked 16

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