
Jasmin Blanchette
ジャスミン・ブランシェット 亚斯麦·布兰切特


I am an assistant professor in the Theoretical Computer Science section of
the Vrije Universiteit Amsterdam, in the Netherlands.
I am also a guest researcher in the VeriDis group at Loria in Nancy, France, and in the Automation
of Logic group at the MaxPlanckInstitut für
Informatik in Saarbrücken, Germany.
I was a postdoc at the Chair for
Logic and Verification at the
Technische Universität München, Germany, which I joined in
2008 as a PhD student.
From 2000 to 2008, I worked as software engineer and documentation manager for
Trolltech (now The Qt Company) in Oslo, Norway.
My research focuses on the use of firstorder automatic
theorem provers and model finders to find proofs and counterexamples in
higherorder logic (Sledgehammer, Nitpick,
Nunchaku,
and Matryoshka).
Another aspect of my work is the development of foundational definitional mechanisms for
(co)datatypes and (co)recursive functions.
I am also interested in formalizing classic results and modern research in
automated reasoning (IsaFoL)
and number theory (Lean Forward).
Contents:
Teaching ⋅
Team ⋅
In the Media ⋅
Drafts ⋅
Journal Articles ⋅
Conference Papers ⋅
Workshop Papers ⋅
Workshop Abstracts ⋅
Theses ⋅
Books ⋅
Other Publications ⋅
Formal Proofs ⋅
Software ⋅
Activities ⋅
Videos ⋅
Address
Teaching
During period 2 of 2019–2020, Alexander Bentkamp and I will teach Logical Verification
using Lean at the VU.
During period 2 of 2018–2019, Johannes Hölzl and I taught Logical Verification
using Lean at the VU.
During period 5 of 2016–2017, I taught Logical Verification using Coq at the VU.
During the 2015 summer term, I taught
Concrete
Semantics with Isabelle/HOL at the Universität des Saarlandes with
Mathias Fleury and Daniel Wand.
During the 2012–13, 2013–14, and 2014–15 winter terms, I was the proud
Master of Competition
for the course
Einführung in die Informatik 2
at the Technische Universität München.
Team
Current members:
 Gabriel Ebner (postdoc, proof automation and formalization of mathematics)
 Robert Y. Lewis (postdoc, formalization of mathematics and proof automation)
 Anne Baanen (PhD student, formalization and automation of mathematics)
 Alexander Bentkamp (PhD student, higherorder reasoning)
 Antoine Defourné (PhD student, a hammer for TLAPS; cosupervisors: Stephan Merz and Pascal Fontaine)
 Daniel El Ouraoui (PhD student, higherorder SMT; cosupervisor: Pascal Fontaine)
 Jannis Limperg (PhD student, automation of mathematics)
 Visa Nummelin (PhD student, higherorder reasoning)
 HansJörg Schurr (PhD student, higherorder SMT; cosupervisor: Pascal Fontaine)
 Petar Vukmirović (PhD student, implementation of λfree higherorder superposition)
Former members:
 Simon Cruanes (senior software engineer, counterexample generation)
 Johannes Hölzl (postdoc, formalization of mathematics and proof automation)
 Mathias Fleury (PhD and MSc student, formalization of inference systems; cosupervisor: Christoph Weidenbach)
 Anders Schlichtkrull (PhD and MSc student, formalization of logical calculi; cosupervisors: Jørgen Villadsen and Thomas Bolander)
 Daniel Wand (PhD student, extensions of superposition; cosupervisor: Christoph Weidenbach)
 Heiko Becker (graduate research immersion lab, higherorder automatic proving)
 Alexander Bentkamp (MSc student, formalization of tensors and deep learning; cosupervisor: Dietrich Klakow)
 Aymeric Bouzy (MSc intern, implementation of corecursion upto; cosupervisor: Dmitriy Traytel)
 Michaël Noël Divo (MSc student, formalization of λcalculi)
 Daniel El Ouraoui (MSc intern, towards higherorder SMT; cosupervisor: Pascal Fontaine)
 Charles Francis (Google Summer of Code, proof redirection)
 Marco Pierre Fernandez Burgos (BSc student, formalization of sorting algorithms in Isabelle/HOL)
 Björn Fischer (MSc student, verification of GPU languages in Lean; cosupervisor: Pieter Hijma)
 Niels Galjaard (BSc student, recursive neural networks for a connection prover)
 Maximilian Haslbeck (MSc directed research, translation of Naproche to Isabelle; cosupervisor: Tobias Nipkow)
 Philipp Hermann (graduate research immersion lab, formalization of tableaux)
 HansDieter Hiep (MSc student, generation of verification conditions for protocols; cosupervisors: Farhad Arbab and Femke van Raamsdonk)
 Kevin Kappelmann (MSc research assistant, formalization of mathematics in Lean; cosupervisor: Sander Dahmen)
 Fabian Kunze (graduate research immersion lab, towards Sledgehammer for Coq)
 Pablo Le Hénaff (MSc intern, Lean formalization and tools; cosupervisors: Johannes Hölzl and Robert Y. Lewis)
 Matthieu Lequesne (MSc internship, TLA^{+} frontend for Nunchaku; cosupervisor: Simon Cruanes)
 Phillip Lippe (MSc research assistant, hammer for Lean; cosupervisors: Robert Y. Lewis)
 Georgi Nakov (MSc project, formalization of redblack trees in Lean)
 Roy Overbeek (MSc student, verification of concurrent revisions; cosupervisor: Wan Fokkink)
 Dmytro Traytel (MSc student, (co)datatype definitions; cosupervisor: Andrei Popescu)
 Petar Vukmirović (MSc student, implementation of λfree higherorder superposition; cosupervisor: Stephan Schulz)
 Max Blans (BSc student, homotopy theory in Agda; cosupervisor: Benno van den Berg)
 Markos Dermitzakis (BSc student, formalization in Lean; cosupervisor: Robert Y. Lewis)
 Martin Desharnais (BEng intern, properties of (co)datatypes; cosupervisor: Dmitriy Traytel)
 Yuan Gao (BSc research assistant, genetic algorithms for time slicing)
 Lorenz Panny (BSc student, (co)recursive function definitions; cosupervisor: Dmitriy Traytel)
 Steffen Juilf Smolka (BSc student, structured Isabelle proofs from refutation proofs)
 Albert Steckermeier (BSc student, enhanced integration of Waldmeister in Sledgehammer)
 Jens Wagemaker (BSc student, formalization of mathematics in Lean; cosupervisors: Johannes Hölzl and Sander Dahmen)
In the Media
 I/O magazine
April 2019. Computer houdt wiskundigen op het rechte pad. By Bennie Mols. Pages 22–24.
Issue (PDF)
Drafts

Superposition for lambdafree higherorder logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann.
Draft article (PDF)
Journal Articles

Formalizing Bachmair and Ganzinger's ordered resolution prover
Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann. Accepted in Journal of Automated Reasoning.
Draft article (PDF)

Scalable finegrained proofs for formula processing
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Accepted in Journal of Automated Reasoning.
Free PDF ⋅ Web site ⋅ Preprint (PDF)

A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Journal of Automated Reasoning 63(2), pp. 347–368, 2019.
Free PDF ⋅ Web site ⋅ Postprint (PDF)

A verified SAT solver framework with learn, forget, restart, and incrementality
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. Journal of Automated Reasoning 61(1–4), pp. 333–365, 2018.
Free PDF ⋅ Web page ⋅ Postprint (PDF)

Introduction to Milestones in Interactive Theorem Proving
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu, and Gregor Snelting. Journal of Automated Reasoning 61(1–4), pp. 1–8, 2018.
Web page ⋅ Postprint (PDF)

A decision procedure for (co)datatypes in SMT solvers
Andrew Reynolds and Jasmin Christian Blanchette Journal of Automated Reasoning
58(3), pp. 341–362, 2017.
Free PDF ⋅ Web page ⋅ Postprint (PDF)

Soundness and completeness proofs by coinductive methods
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Journal of Automated Reasoning
58(1), pp. 149–179, 2017.
Free PDF ⋅ Web page ⋅ Postprint (PDF)

Encoding monomorphic and polymorphic types
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone.
Logical Methods in Computer Science 12(4:13), 2016, pp. 1–52.
Postprint (PDF)

A learningbased fact selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban.
Journal of Automated Reasoning 57(3), pp. 219–244, 2016.
Free PDF ⋅ Web page ⋅ Postprint (PDF)

Semiintelligible Isar proofs from machinegenerated proofs
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier.
Journal of Automated Reasoning 56(2), pp. 155–200, 2016.
Web page ⋅ Postprint (PDF)

Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban.
Journal of Formalized Reasoning 9(1), pp. 101–148, 2016.
Web page ⋅ Postprint (PDF)

Extending Sledgehammer with SMT solvers
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson.
Journal of Automated Reasoning 51(1), pp. 109–128, 2013.
Web page
⋅
Postprint (PDF)

LEOII and Satallax on the Sledgehammer test bench
Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson.
Journal of Applied Logic 11(1), pp. 91–102, 2013.
Web page
⋅
Postprint (PDF)
 Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
Jasmin Christian Blanchette Software Quality Journal 21(1), pp. 101–126, 2013.
Web page
⋅
Postprint (PDF)
 Monotonicity inference for higherorder formulas
Jasmin Christian Blanchette and Alexander Krauss. Journal of Automated Reasoning 47(4), pp. 369–398, 2011.
Web page
⋅
Postprint (PDF)
 Proof pearl: Mechanizing the textbook proof of
Huffman's algorithm in Isabelle/HOL
Jasmin Christian Blanchette Journal of Automated Reasoning 43(1), pp. 1–18, 2009.
Web page
⋅
Postprint (PDF)
Conference Papers

Superposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE27), LNCS 11716, pp. 55–73, Springer, 2019.
Web page ⋅ Draft paper (PDF) ⋅ Report (PDF)

Extending a brainiac prover to lambdafree higherorder logic
Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz.
In Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2019), LNCS 11427, pp. 192–210, Springer, 2019.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

A verified prover based on ordered resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 152–165, ACM, 2019.
Web page ⋅ PDF

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)
Jasmin Christian Blanchette In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 1–13, ACM, 2019.
Web page ⋅ PDF

Bindings as bounded natural functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. In PAMPL 3(POPL), pp. 22:1–22:34, 2019.
Web page ⋅ PDF ⋅ Report (PDF)

Superposition with datatypes and codatatypes
Jasmin Christian Blanchette, Nicolas Peltier, and Simon Robillard.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018),
LNCS 10900, pp. 370–387, Springer, 2018.
Web page
⋅ Postprint (PDF) ⋅ Report (PDF)

Superposition for lambdafree higherorder logic
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018),
LNCS 10900, pp. 28–46, Springer, 2018.
Web page
⋅ Postprint (PDF) ⋅ Report (PDF)

Formalizing Bachmair and Ganzinger's ordered resolution prover
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018),
LNCS 10900, pp. 89–107, Springer, 2018.
Web page
⋅ Postprint (PDF) ⋅ Report (PDF)

A verified SAT solver with watched literals using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. In Andronick, J., Felty, A. P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 158–171, ACM, 2018.
Postprint (PDF)

Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel.
In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017),
LIPIcs 84, pages 11:1–11:18, Schloss Dagstuhl—LeibnizZentrum für Informatik, 2017.
Postprint (PDF)

A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
In AyalaRincón, M., Muños, C. A. (eds.) 8th Conference on Interactive Theorem Proving (ITP 2017),
LNCS 10499, pp. 46–64, Springer, 2017.
Web page ⋅ Postprint (PDF)

A verified SAT solver framework with learn, forget, restart, and incrementality
Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach.
In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI17), pp. 4786–4790, ijcai.org, 2017.
Web page ⋅ Postprint (PDF)

Foundational (co)datatypes and (co)recursion for higherorder logic
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin
Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas
Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel,
René Thiemann, and Dmitriy Traytel.
In Dixon, C., Finger, M. (eds.)
11th International Symposium on Frontiers of Combining Systems (FroCoS 2017),
LNCS 10483, pp. 3–21, Springer, 2017.
Web page
⋅
Postprint (PDF)

A transfinite Knuth–Bendix order for lambdafree higherorder terms
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand.
In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE26), LNCS 10395, pp. 432–453, Springer, 2017.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

Scalable finegrained proofs for formula processing
Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine.
In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE26), LNCS 10395, pp. 398–412, Springer, 2017.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

Foundational nonuniform (co)datatypes for higherorder logic
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, and Dmitriy Traytel.
32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), pp. 1–12, IEEE Computer Society, 2017.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

A lambdafree higherorder recursive path order
Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand.
In Esparza, J., Murawski, A. S. (eds.) 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), LNCS 10203, pp. 461–479, Springer, 2017.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

Friends with benefits: Implementing corecursion in foundational proof assistants
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel.
In Yang, H. (ed.) 26th European Symposium on Programming (ESOP 2017), LNCS 10201, pp. 111–140, Springer, 2017.
Web page ⋅ Postprint (PDF) ⋅ Report (PDF)

A decision procedure for (co)datatypes in SMT solvers
Andrew Reynolds and Jasmin Christian Blanchette
In Kambhampati, S. (ed.) 25th International Joint Conference on Artificial Intelligence (IJCAI16), pp. 4205–4209, IJCAI/AAAI Press, 2016.
Web page ⋅ Postprint (PDF)

A verified SAT solver framework with learn, forget, restart, and incrementality
Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. In Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016),
LNCS 9706, pp. 25–44, Springer, 2016.
Postprint (PDF)

Model finding for recursive functions in SMT
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli. In Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016),
LNCS 9706, pp. 133–151, Springer, 2016.
Postprint (PDF)

Foundational extensible corecursion—A proof assistant perspective
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Fisher, K., Reppy, J. H. (eds.) 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015),
pp. 192–204, ACM, 2015.
Postprint (PDF)

A decision procedure for (co)datatypes in SMT solvers
Andrew Reynolds and Jasmin Christian Blanchette In Felty, A., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE25),
LNCS 9195, pp. 197–213, Springer, 2015.
Postprint (PDF)
⋅
Report (PDF)

Mining the Archive of Formal Proofs
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. In Kerber, M. (ed.) International Conference on Intelligent Computer Mathematics (CICM 2015),
LNCS 9150, pp. 1–15, Springer, 2015.
Postprint (PDF)

Witnessing (co)datatypes
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Vitek, J. (ed.)
European Symposium on Programming (ESOP 2015),
LNCS 9032, pp. 359–382, Springer, 2015.
Postprint (PDF)

Experience report: The next 1100 Haskell programmers
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, and Dmitriy Traytel.
In Jeuring, J., Chakravarty, M. M. T. (eds.) ACM SIGPLAN Haskell Symposium 2014 (Haskell 2014), pp. 25–30, ACM, 2014.
Web page
⋅
Postprint (PDF)

Truly modular (co)datatypes for Isabelle/HOL
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. In Klein, G., Gamboa, R. (eds.)
5th Conference on Interactive Theorem Proving (ITP 2014),
LNCS 8558, pp. 93–110, Springer, 2014.
Web page
⋅
Postprint (PDF)

Cardinals in Isabelle/HOL
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Klein, G., Gamboa, R. (eds.)
5th Conference on Interactive Theorem Proving (ITP 2014),
LNCS 8558, pp. 111–127, Springer, 2014.
Web page
⋅
Postprint (PDF)

Unified classical logic completeness: A coinductive pearl
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In
Demri, S., Kapur, D., Weidenbach, C. (eds)
7th International Joint Conference on Automated Reasoning (IJCAR 2014),
LNCS 8562, pp. 46–60, Springer, 2014.
Web page
⋅
Postprint (PDF)

Mechanizing the metatheory of Sledgehammer
Jasmin Christian Blanchette and Andrei Popescu. In Fontaine, P., Ringeissen, C., Schmidt, R. A. (eds.)
9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
LNCS 8152, pp. 245–260, Springer, 2013.
Web page
⋅
Postprint (PDF)

MaSh: Machine learning for Sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban.
In Blazy, S., PaulinMohring, C., Pichardie, D. (eds.)
4th Conference on Interactive Theorem Proving (ITP 2013),
LNCS 7998, pp. 35–50, Springer, 2013.
Web page
⋅
Postprint (PDF)

TFF1: The TPTP typed firstorder form with rank1 polymorphism (system description)
Jasmin Christian Blanchette and Andrei Paskevich. In Bonacina, M. P. (ed.) 24th International Conference on Automated Deduction (CADE24),
LNCS 7898, pp. 414–420, Springer, 2013.
Web page
⋅
Postprint (PDF) ⋅ Specification (PDF)

Encoding monomorphic and polymorphic types
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone.
In Piterman, N., Smolka, S. (eds.) 19th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2013), LNCS 7795, pp. 493–507, Springer, 2013.
Web page
⋅ Postprint (PDF)

Foundational, compositional (co)datatypes for higherorder logic—Category theory applied to theorem proving
Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette In
27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012),
pp. 596–605, IEEE Computer Society, 2012.
Web page
⋅
Postprint (PDF)

More SPASS with Isabelle—Superposition with hard sorts and configurable simplification
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. In Beringer, L., Felty, A. P. (eds.) Third International Conference on Interactive Theorem Proving (ITP 2012),
LNCS 7406, pp. 345–360, Springer, 2012.
Web page
⋅
Postprint (PDF)

Automatic proof and disproof in Isabelle/HOL
Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. In Tinelli, C., SofronieStokkermans, V. (eds.) 8th International Symposium
Frontiers of Combining Systems (FroCoS 2011),
LNCS 6989, pp. 12–27, Springer, 2011.
Web page
⋅
Postprint (PDF)

Extending Sledgehammer with SMT solvers
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson.
In Bjørner, N., SofronieStokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE23),
LNCS 6803, pp. 116–130, Springer, 2011.
Web page
⋅
Postprint (PDF)

Nitpicking C++ concurrency
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar.
13th International ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming (PPDP 2011),
pp. 113–124, ACM, 2011.
Web page
⋅ Postprint (PDF)

Generating counterexamples for structural inductions by exploiting nonstandard models
Jasmin Christian Blanchette and Koen Claessen.
In Fermüller, C. G., Voronkov, A. (eds.) 17th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010),
LNCS 6397, pp. 117–141, Springer, 2010.
Web page
⋅
Postprint (PDF)
 Nitpick: A counterexample generator for Isabelle/HOL based on the relational
model finder Kodkod (system description)
Jasmin Christian Blanchette Presented at the 17th International
Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR
Yogyakarta 2010).
Web page
⋅ Postprint (PDF)

Monotonicity inference for higherorder formulas
Jasmin Christian Blanchette and Alexander Krauss.
In Giesl, J., Hähnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010),
LNCS 6173, pp. 91–106, Springer, 2010.
Web page ⋅
Postprint (PDF)

Nitpick: A counterexample generator for higherorder logic based on a
relational model finder
Jasmin Christian Blanchette and Tobias Nipkow.
In Kaufmann, M., Paulson, L. C. (eds.)
First International Conference on Interactive Theorem Proving (ITP 2010), LNCS 6172, pp. 131–146, Springer, 2010.
Web page ⋅
Postprint (PDF)

Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
Jasmin Christian Blanchette
In Fraser, G., Gargantini, A. (eds.) Fourth International Conference on Tests and Proofs (TAP 2010), LNCS 6143, pp. 117–134, Springer, 2010.
Web page ⋅
Postprint (PDF)

Nitpick: A counterexample generator for higherorder logic based on a
relational model finder (extended abstract)
Jasmin Christian Blanchette and Tobias Nipkow. Third International
Conference on Tests and Proofs (TAP 2009). In Dubois, C. (ed.) TAP 2009:
Short Papers, ETH Technical Report 630, 2009.
Full proceedings (PDF) ⋅
Postprint (PDF)
Workshop Papers

Language and proofs for higherorder SMT (work in progress)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine.
In Dubois, C., Woltzenlogel Paleo, B. (eds.) 5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017), pp. 15–22, EPTCS 262, 2017.
Web page ⋅ Postprint (PDF)

Extending Nunchaku to dependent type theory
Simon Cruanes and Jasmin Christian Blanchette Hammers for Type Theories (HaTT 2016)
Postprint (PDF)

Model finding for recursive functions in SMT
Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. In Ganesh, V., Jovanović, D. (eds.) Satisfiability Modulo Theories Workshop (SMT 2015).
Postprint (PDF) ⋅
Report (PDF)

Primitively (co)recursive definitions for Isabelle/HOL
Lorenz Panny, Jasmin Christian Blanchette, and Dmitriy Traytel. Isabelle Workshop 2014.
Postprint (PDF)

My life with an automatic theorem prover
Jasmin Christian Blanchette In Kovács, L., Voronkov, A. (eds.) First and Second Vampire Workshops (Vampire 2014 and 2015), pp. 1–7, EPiC 38, EasyChair, 2016.
Postprint (PDF)

A survey of axiom selection as a machine learning problem
Jasmin Christian Blanchette and Daniel Kühlwein. In Geschke, S., Loewe, B., Schlicht, P. (eds.) Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter Koepke and Philip Welch, Tributes, College Publications, 2014.
Postprint (PDF)

Robust, semiintelligible Isabelle proofs from ATP proofs
Steffen Juilf Smolka and Jasmin Christian Blanchette In Blanchette, J. C., Urban, J. (eds.) Third International Workshop on
Proof Exchange for Theorem Proving (PxTP 2013), pp. 117–132, EPiC 14, EasyChair, 2013.
Postprint (PDF)

Redirecting proofs by contradiction
Jasmin Christian Blanchette In Blanchette, J. C., Urban, J. (eds.) Third International Workshop on
Proof Exchange for Theorem Proving (PxTP 2013), pp. 11–26, EPiC 14, EasyChair, 2013.
Postprint (PDF)
 Three years of experience with Sledgehammer, a practical link between automated and
interactive theorem provers
Lawrence C. Paulson and Jasmin Christian Blanchette 8th International Workshop on the Implementation of Logics (IWIL2010).
Full proceedings (PDF) ⋅
Postprint (PDF)

Intraobject versus interobject: Concurrency and reasoning in Creol
Einar Broch Johnsen, Jasmin Christian Blanchette, Marcel Kyas, and Olaf Owe.
Electronic Notes in Theoretical Computer
Science 243 (2nd International Workshop on Harnessing Theories for Tool Support in Software,
TTSS 2008), pp. 89–103, 2009.
Web page ⋅
Postprint (PDF)
 An open system operational
semantics for an objectoriented and componentbased language
Jasmin Christian Blanchette and Olaf Owe. Electronic
Notes in Theoretical Computer Science 215 (4th
International Workshop on Formal Aspects of Component Software, FACS 2007), pp.
151–169, 2008.
Web page ⋅
Postprint (PDF)
Workshop Abstracts

Stronger HigherOrder Automation: A Report on the Ongoing Matryoshka Project
Jasmin Blanchette, Pascal Fontaine, Stephan Schulz, Sophie Tourret, and Uwe Waldmann. Accepted at Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019).
Preprint (PDF)

Better SMT proofs for easier reconstruction
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, and HansJörg Schurr. In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
Preprint (PDF)

Machine learning for instance selection in SMT solving
Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine, and Cezary Kaliszyk. In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
Preprint (PDF)

A verified SAT solver with watched literals using Imperative HOL (extended abstract)
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. In Nipkow, T., Paulson, L., Wenzel, M. (eds.) Isabelle Workshop 2018.
PDF

Towards strong higherorder automation for fast interactive verification
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, and Uwe Waldmann.
In Reger, G., Traytel, D. (eds.) 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017), pp. 16–23, EPiC 51, EasyChair, 2017.
Web page ⋅ Postprint (PDF)

An Isabelle formalization of the expressiveness of deep learning (extended abstract)
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Hales, T. C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017), pp. 22–23.
Postprint (PDF)

Friends with benefits: Implementing foundational corecursion in Isabelle/HOL (extended abstract)
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Isabelle Workshop 2016.
Postprint (PDF)

A verified SAT solver framework with learn, forget, restart, and incrementality (extended abstract)
Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. Isabelle Workshop 2016.
Postprint (PDF)

Model finding for recursive functions in SMT
Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. QUANTIFY 2015.
Postprint (PDF)

Toward Nitpick and Sledgehammer for Coq
Jasmin Christian Blanchette Coq Workshop 2015.
Postprint (PDF)

Isabelle and security
Jasmin Christian Blanchette and Andrei Popescu. Grande Region Security and Reliability Day 2015, presented
at poster session.
Postprint (PDF)
Theses
 Automatic Proofs and Refutations for HigherOrder Logic
Jasmin Christian Blanchette PhD thesis, Fakultät für Informatik,
Technische Universität München, June 2012.
PDF
 Verification of Assertions in Creol Programs
Jasmin Christian Blanchette MSc thesis, Institutt for informatikk, Universitetet i Oslo, May 2008.
PDF
Books

Seventh International Conference on Interactive Theorem Proving (ITP 2016)
Jasmin Christian Blanchette and Stephan Merz (eds.)
LNCS 9807, Springer, 2016.
Web page

First International Workshop on Hammers for Type Theories (HaTT 2016)
Jasmin Christian Blanchette and Cezary Kaliszyk (eds.)
EPTCS 210, 2016.
Web page
⋅ PDF

Ninth International Conference on Tests and Proofs (TAP 2015)
Jasmin Christian Blanchette and Nikolai Kosmatov (eds.)
LNCS 9154, Springer, 2015.
Web page

Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013)
Jasmin Christian Blanchette and Josef Urban (eds.)
EPiC 14, EasyChair, 2013.
Web page
⋅ PDF
 C++ GUI Programming with Qt 4
(Second Edition)
J. B. and Mark Summerfield. Prentice Hall Open Source Software Development Series,
Prentice Hall, February 2008.
Chinese (Simplified), German, Korean, and Russian translations are available.
Web page
 C++ GUI Programming with Qt 4
J. B. and Mark Summerfield. Prentice Hall, July 2006.
Chinese (Simplified), French, German, Japanese, and Russian
translations are available.
Web page ⋅
PDF
 C++ GUI Programming with Qt 3
J. B. and Mark Summerfield. Bruce
Perens' Open Source Series, Prentice Hall, January 2004.
Chinese (Simplified), German, Japanese, and Russian translations are available.
Web page ⋅
PDF
Other Publications

Monotonicity or how to encode polymorphic types safely and efficiently
Jasmin Christian Blanchette, Sascha Böhme, and Nicholas Smallbone. Subsumed by “Encoding monomorphic and polymorphic types.”
Technical report (PDF)
 The Little Manual of API Design
J. B. Trolltech, a Nokia company, June 2008.
PDF
 Overview of the Creol language
Jasmin Christian Blanchette Essay, Department of Informatics, Univerity of Oslo, May 2007.
PDF
 Throwing MFC out of Windows—Qt application
development with Visual Studio .NET
J. B. Linux Magazine 73, pp. 40–43, December 2006.
Web page
 WindowstoLinux migration with Qt
J. B. TUX 4, July 2005.
Web page
Formal Proofs

A verified functional implementation of Bachmair and Ganzinger's ordered resolution prover
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. Archive of Formal Proofs, 2018.
Web page

Formalization of Bachmair and Ganzinger's ordered resolution prover
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Archive of Formal Proofs, 2018.
Web page

Operations on bounded natural functors
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2018.
Web page

Abstract soundness
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2017.
Web page

Formalization of Knuth–Bendix orders for lambdafree higherorder terms
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016.
Web page

Formalization of nested multisets, hereditary multisets, and syntactic ordinals
Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Archive of Formal Proofs, 2016.
Web page

Formalization of recursive path orders for lambdafree higherorder terms
Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016.
Web page

Abstract completeness
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2014.
Web page

Sound and complete sort encodings for firstorder logic
Jasmin Christian Blanchette and Andrei Popescu. Archive of Formal Proofs, 2013.
Web page

The textbook proof of Huffman's algorithm
Jasmin Christian Blanchette. Archive of Formal Proofs, 2008.
Web page
Software

Nunchaku—A standalone higherorder model finder.
Repository

Isabelle's (co)datatype package—Commands for defining (co)datatypes and primitively (co)recursive functions.
User's manual (PDF)

Sledgehammer—Let automatic theorem provers write your Isabelle/HOL proof scripts.
User's manual (PDF)
Activities
 Steering committee member: CPP (2019–), CADE trustee (2016–2019), ITP (2016–), TAP (2015–).
 AAR newsletter editor and board member (2015–2017).
 Conference program committee member:
CSL 2021,
LPAR 2020,
IJCAR 2020,
TAP 2020,
TACAS 2020,
CPP 2020 (cochair),
FMCAD 2019,
PPDP 2019,
FroCoS 2019,
CADE27,
NFM 2018,
CAV 2018,
TAP 2018,
IJCAR 2018,
ITP 2018,
CPP 2018,
CAV 2017,
CADE26,
TAP 2017,
ITP 2016 (cochair),
TAP 2016,
TAP 2015 (cochair),
CADE25,
IJCAR 2014,
FroCoS 2013.
 Conference organization:
ITP 2016 (coorganizer),
CADE25 (cochair of workshops, tutorials, and competitions).
 Workshop program committee member:
AITP 2020,
DeMent 2019,
ARCADE 2019,
Deduktionstreffen 2019,
AITP 2019,
IWIL2018,
Deduktionstreffen 2018,
VDMW 2018,
AITP 2018,
SMT 2017,
PxTP 2017,
IWIL2017,
ARCADE 2017,
AITP 2017,
Deduktionstreffen 2016,
SMT 2016,
HaTT 2016 (cochair),
QBF 2016,
IWIL2015,
LSFA 2015,
QUANTIFY 2015,
Deduktionstreffen 2015,
PxTP 2015,
PAAR2014,
PxTP 2013 (cochair),
PxTP 2012,
IWIL2012,
PAAR2012, and
IWIL2010.
Videos
 Inria Inside—Jasmin Blanchette, 2016.
YouTube
 Qt 4 Dance, 2005. JeanClaude, c'est moi.
YouTube
Address
Dr. J. C. Blanchette
NU Building, office NU12A65
Vrije Universiteit Amsterdam
Department of Computer Science
Section of Theoretical Computer Science
De Boelelaan 1081a
1081 HV Amsterdam
The NetherlandsPhone: +31 20 598 3306
Email: j.c.blanchette vu.nl
“A proof is a proof.
What kind of a proof?
It's a proof.
A proof is a proof,
and when you have a good proof,
it's because it's proven.”
— Jean Chrétien

