Jasmin Christian Blanchette

According to our database1, Jasmin Christian Blanchette authored at least 76 papers between 2006 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Introduction to the STAF 2015 special section.
Software and System Modeling, 2019

Bindings as bounded natural functors.
PACMPL, 2019

Selected Extended Papers of ITP 2016: Preface.
J. Autom. Reasoning, 2019

Extending a Brainiac Prover to Lambda-Free Higher-Order Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

A verified prover based on ordered resolution.
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).
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.
J. Autom. Reasoning, 2018

Introduction to Milestones in Interactive Theorem Proving.
J. Autom. Reasoning, 2018

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover.
Archive of Formal Proofs, 2018

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover.
Archive of Formal Proofs, 2018

A verified SAT solver with watched literals using imperative HOL.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Superposition with Datatypes and Codatatypes.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Superposition for Lambda-Free Higher-Order Logic.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Soundness and Completeness Proofs by Coinductive Methods.
J. Autom. Reasoning, 2017

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

Language and Proofs for Higher-Order SMT (Work in Progress).
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Operations on Bounded Natural Functors.
Archive of Formal Proofs, 2017

Abstract Soundness.
Archive of Formal Proofs, 2017

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Foundational nonuniform (Co)datatypes for higher-order logic.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

A Formal Proof of the Expressiveness of Deep Learning.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

A Lambda-Free Higher-Order Recursive Path Order.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.
Proceedings of the Programming Languages and Systems, 2017

Towards Strong Higher-Order Automation for Fast Interactive Verification.
Proceedings of the ARCADE 2017, 2017

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms.
Proceedings of the Automated Deduction - CADE 26, 2017

Scalable Fine-Grained Proofs for Formula Processing.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Hammering towards QED.
J. Formalized Reasoning, 2016

A Learning-Based Fact Selector for Isabelle/HOL.
J. Autom. Reasoning, 2016

Semi-intelligible Isar Proofs from Machine-Generated Proofs.
J. Autom. Reasoning, 2016

Extending Nunchaku to Dependent Type Theory.
Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms.
Archive of Formal Proofs, 2016

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals.
Archive of Formal Proofs, 2016

Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms.
Archive of Formal Proofs, 2016

A Decision Procedure for (Co)datatypes in SMT Solvers.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Model Finding for Recursive Functions in SMT.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381).
Dagstuhl Reports, 2015

Mining the Archive of Formal Proofs.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Foundational extensible corecursion: a proof assistant perspective.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Witnessing (Co)datatypes.
Proceedings of the Programming Languages and Systems, 2015

A Decision Procedure for (Co)datatypes in SMT Solvers.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Abstract Completeness.
Archive of Formal Proofs, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Cardinals in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Experience report: the next 1100 Haskell programmers.
Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

My Life with an Automatic Theorem Prover.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

Unified Classical Logic Completeness - A Coinductive Pearl.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
LEO-II and Satallax on the Sledgehammer test bench.
J. Applied Logic, 2013

Sound and Complete Sort Encodings for First-Order Logic.
Archive of Formal Proofs, 2013

Encoding Monomorphic and Polymorphic Types.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

MaSh: Machine Learning for Sledgehammer.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Mechanizing the Metatheory of Sledgehammer.
Proceedings of the Frontiers of Combining Systems, 2013

Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.
Proceedings of the Automated Deduction - CADE-24, 2013

Redirecting Proofs by Contradiction.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
Automatic proofs and refutations for higher-order logic.
PhD thesis, 2012

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011
Nitpicking C++ concurrency.
Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Automatic Proof and Disproof in Isabelle/HOL.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Extending Sledgehammer with SMT Solvers.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions.
Proceedings of the Tests and Proofs, 4th International Conference, 2010

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.
Proceedings of the 8th International Workshop on the Implementation of Logics, 2010

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models.
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.
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.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Monotonicity Inference for Higher-Order Formulas.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.
J. Autom. Reasoning, 2009

Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol.
Electr. Notes Theor. Comput. Sci., 2009

2008
An Open System Operational Semantics for an Object-Oriented and Component-Based Language.
Electr. Notes Theor. Comput. Sci., 2008

The Textbook Proof of Huffman's Algorithm.
Archive of Formal Proofs, 2008

C++ GUI Programming with Qt 4, 2nd Edition.
Pearson Education, ISBN: 978-0-13-235416-5, 2008

2006
C++ GUI programming with Qt 4.
Prentice Hall, ISBN: 0131872494, 2006


  Loading...