
Jasmin Christian Blanchette
ジャスミン・クリスチャン・ブランチェット 亚斯麦·克里斯蒂安·布兰切特
I am a member of the VeriDis group at
Inria Nancy – GrandEst & LORIA, France, and am also hosted by
the Automation of Logic group at
the Max Planck Institute for Informatics
in Saarbrücken, Germany. Until the end of 2014, 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 Ph.D. 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,
and Nunchaku).
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).
Contents:
Teaching ⋅
Supervision ⋅
Drafts ⋅
Journal Articles ⋅
Conference Papers ⋅
Workshop Papers ⋅
Workshop Abstracts ⋅
Theses ⋅
Books ⋅
Other Publications ⋅
Software ⋅
Activities ⋅
Video ⋅
Addresses ⋅
Resume
Teaching
During the 2015 summer term, I was
teaching Concrete
Semantics with Isabelle/HOL at the Universität des Saarlandes with
help from 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.
Supervision
Current
 Simon Cruanes (postdoctoral software engineer, Nitpick's successor Nunchaku)
 Mathias Fleury (Ph.D., formalization of inference systems; cosupervisor: Christoph Weidenbach)
 Anders Schlichtkrull (Ph.D., formalization of logical calculi; main supervisor: Jørgen Villadsen)
 Fabian Kunze (M.Sc. research immersion, Sledgehammer for Coq)
Past
 Philipp Hermann (M.Sc. research immersion, formalization of tableaux)
 Mathias Fleury (M.Sc. intern, integration of provers in Sledgehammer and formalization of ground inference systems; cosupervisor: Dmitriy Traytel)
 Anders Schlichtkrull (M.Sc., formalization of resolution; main supervisor: Jørgen Villadsen)
 Aymeric Bouzy (M.Sc. intern, implementation of corecursion upto; cosupervisor: Dmitriy Traytel)
 Martin Desharnais (B.Eng. intern, properties of (co)datatypes; cosupervisor: Dmitriy Traytel)
 Albert Steckermeier (B.Sc., enhanced integration of Waldmeister in Sledgehammer)
 Maximilian Haslbeck (M.Sc. directed research, translation of Naproche to Isabelle; main supervisor: Tobias Nipkow)
 Lorenz Panny (B.Sc., (co)recursive function definitions; cosupervisor: Dmitriy Traytel)
 Steffen Juilf Smolka (B.Sc., structured Isabelle proofs from refutation proofs)
 Dmytro Traytel (M.Sc., (co)datatype definitions; main supervisor: Andrei Popescu)
 Charles Francis (Google Summer of Code, proof redirection)
 Yuan Gao (B.Sc. research assistant, genetic algorithms for time slicing)
Drafts

A decision procedure for (co)datatypes in SMT solvers
Andrew Reynolds and J. C. B.
Draft article (PDF)

Soundness and completeness proofs by coinductive methods
J. C. B., Andrei Popescu, and Dmitriy Traytel.
Submitted article (PDF)
Journal Articles

Encoding monomorphic and polymorphic types
J. C. B., Sascha Böhme, Andrei Popescu, and Nicholas Smallbone.
Accepted in Logical Methods in Computer Science.
Submitted article (PDF)

Hammering towards QED
J. C. B., Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban.
To appear in Journal of Formalized Reasoning.
Preprint (PDF)

Semiintelligible Isar proofs from machinegenerated proofs
J. C. B., Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. To appear in Journal of Automated Reasoning.
Preprint (PDF)

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

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

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

Mining the Archive of Formal Proofs
J. C. B., Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. In Kerber, M. (ed.) International Conference on Intelligent Computer Mathematics (CICM 2015),
LNAI 9150, pp. 1–15, Springer, 2015.
Preprint (PDF)

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

Experience report: The next 1100 Haskell programmers
J. C. B., 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 Press, 2014.
Web page
⋅
Preprint (PDF)

Truly modular (co)datatypes for Isabelle/HOL
J. C. B., 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
⋅
Preprint (PDF)

Cardinals in Isabelle/HOL
J. C. B., 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
⋅
Preprint (PDF)

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

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

MaSh: Machine learning for Sledgehammer
Daniel Kühlwein, J. C. B., 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
⋅
Preprint (PDF)

TFF1: The TPTP typed firstorder form with rank1 polymorphism (system description)
J. C. B. and Andrei Paskevich. In Bonacina, M. P. (ed.) 24th International Conference on Automated Deduction (CADE24),
LNAI 7898, pp. 414–420, Springer, 2013.
Web page
⋅
Preprint (PDF) ⋅ Draft specification (PDF)

Encoding monomorphic and polymorphic types
J. C. B., 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
⋅ Preprint (PDF)

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

More SPASS with Isabelle—Superposition with hard sorts and configurable simplification
J. C. B., 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
⋅
Preprint (PDF)

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

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

Nitpicking C++ concurrency
J. C. B., 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 Press, 2011.
Web page
⋅ Preprint (PDF)

Generating counterexamples for structural inductions by exploiting nonstandard models
J. C. B. 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),
LNAI 6397, pp. 117–141, Springer, 2010.
Web page
⋅
Preprint (PDF)
 Nitpick: A counterexample generator for Isabelle/HOL based on the relational
model finder Kodkod (system description)
J. C. B. Presented at the 17th International
Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR
Yogyakarta 2010).
Web page
⋅ Preprint (PDF)

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

Nitpick: A counterexample generator for higherorder logic based on a
relational model finder
J. C. B. 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 ⋅
Preprint (PDF)

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

Nitpick: A counterexample generator for higherorder logic based on a
relational model finder (extended abstract)
J. C. B. 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) ⋅
Preprint (PDF)
Workshop Papers

Primitively (co)recursive definitions for Isabelle/HOL
Lorenz Panny, J. C. B., and Dmitriy Traytel. Isabelle Workshop 2014.
Preprint (PDF)

My life with an automatic theorem prover
J. C. B. Vampire 2014.
Preprint (PDF)

Axiom selection as a machine learning problem
J. C. B. and Daniel Kühlwein. In Geschke, S., Loewe, B., and Schlicht, P., Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter Koepke and Philip Welch, Tributes, College Publications, 2014.
Preprint (PDF)

Robust, semiintelligible Isabelle proofs from ATP proofs
Steffen Juilf Smolka and J. C. B. Third International Workshop on
Proof Exchange for Theorem Proving (PxTP 2013).
Preprint (PDF)

Redirecting proofs by contradiction
J. C. B. Third International Workshop on
Proof Exchange for Theorem Proving (PxTP 2013).
Preprint (PDF)
 Three years of experience with Sledgehammer, a practical link between automated and
interactive theorem provers
Lawrence C. Paulson and J. C. B. 8th International Workshop on the Implementation of Logics (IWIL2010).
Full proceedings (PDF) ⋅
Preprint (PDF)

Intraobject versus interobject: Concurrency and reasoning in Creol
Einar Broch Johnsen, J. C. B., 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 ⋅
Preprint (PDF)
 An open system operational
semantics for an objectoriented and componentbased language
J. C. B. 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 ⋅
Preprint (PDF)
Workshop Abstracts

Toward Nitpick and Sledgehammer for Coq
J. C. B. Coq Workshop 2015.
Abstract (PDF)

Isabelle and security
J. C. B. and Andrei Popescu. Grande Region Security and Reliability Day 2015, accepted for
poster session.
Abstract (PDF)
Theses
 Verification of Assertions in Creol Programs
J. C. B. M.Sc. thesis, Institutt for informatikk, Universitetet i Oslo, May 2008.
PDF
Books
 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

Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013)
J. C. B. and Josef Urban (eds.)
EPiC 14, EasyChair, 2013.
Web page
⋅ PDF

Monotonicity or how to encode polymorphic types safely and efficiently
J. C. B., Sascha Böhme, and Nicholas Smallbone. Subsumed by “Encoding monomorphic and polymorphic types.”
Technical report (PDF)
 An Isabelle/HOL formalization of
the textbook proof of Huffman's algorithm
J. C. B. In Klein, G., Nipkow, T., Paulson, L. (eds.),
Archive of Formal Proofs, October 2008.
Web page
⋅
PDF
 The Little Manual of API Design
J. B. Trolltech, a Nokia company, June 2008.
PDF
 Overview of the Creol language
J. C. B. 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 ⋅ PDF
Software

DiffPDF—A utility to compare PDFs. Developed by Mark Summerfield.
Web page
Activities
 AAR newsletter editor and board member.
 Program committee member, conferences:
ITP 2016 (cochair),
TAP 2016,
TAP 2015 (cochair),
CADE25 (cochair of workshops, tutorials, and competitions),
IJCAR 2014,
FroCoS 2013.
 Program committee member, workshops:
HaTT 2016 (cochair),
IWIL 2015,
LSFA 2015,
QUANTIFY 2015,
Deduktionstreffen 2015,
PxTP 2015,
PAAR2014,
PxTP 2013 (cochair),
PxTP 2012,
IWIL 2012,
PAAR2012, and
IWIL 2010.
Video
Addresses
Nancy
Jasmin Blanchette
Inria Nancy – GrandEst & LORIA
Équipe VeriDis, Room B223
615, rue du Jardin Botanique
54600 VillerslèsNancy
FrancePhone: +33 (0)3 83 59 30 40
Fax: +33 (0)3 83 41 30 79
Email: jasmin.blanchette inria.fr
Email: jasmin.blanchette loria.fr

Saarbrücken
Dr. Jasmin Blanchette
MaxPlanckInstitut für Informatik
Automation of Logic Group
Campus E1 4, Building E1 5, Room 621
66123 Saarbrücken
GermanyPhone: +49 (0)681 9325 2915
Fax: +49 (0)681 9325 2999
Email: jasmin.blanchette mpiinf.mpg.de
Email: jasmin.blanchette mpiinf.mpg.de

“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

