Jasmin Christian 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 Max-Planck-Institut 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 first-order automatic theorem provers and model finders to find proofs and counterexamples in higher-order 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).


News

  • My colleagues Robert Y. Lewis and Johannes Hölzl will be organizing Lean Together 2019, a get-together for mathematically oriented Lean users.

Contents:  TeachingSupervisionDraftsJournal ArticlesConference PapersWorkshop PapersWorkshop AbstractsThesesBooksOther PublicationsFormal ProofsSoftwareActivitiesVideosAddress


Teaching

During period 2 of 2018–2019, Johannes Hölzl and I are teaching 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.


Supervision

Note to students: Please send me an email if you are interested in working under my supervision. See also the Lean Forward and Matryoshka project pages.

Current:

  • Alexander Bentkamp (PhD, higher-order reasoning)
  • Markos Dermitzakis (BSc, formalization in Lean; cosupervisors: Robert Y. Lewis and Johannes Hölzl)
  • Daniel El Ouraoui (PhD, higher-order SMT; main supervisor: Pascal Fontaine)
  • Mathias Fleury (PhD, formalization of inference systems; main supervisor: Christoph Weidenbach)
  • Niels Galjaard (BSc, recursive neural networks for a connection prover)
  • Johannes Hölzl (postdoc, formalization of mathematics and proof automation)
  • Robert Y. Lewis (postdoc, formalization of mathematics and proof automation)
  • Phillip Lippe (MSc research assistant, hammer for Lean)
  • Roy Overbeek (MSc, verification of concurrent revisions; main supervisor: Wan Fokkink)
  • Hans-Jörg Schurr (PhD, higher-order SMT; main supervisor: Pascal Fontaine)
  • Petar Vukmirović (PhD, implementation of λ-free higher-order superposition)

Past:

  • Heiko Becker (graduate research immersion lab, higher-order automatic proving)
  • Alexander Bentkamp (MSc, formalization of tensors and deep learning; main supervisor: Dietrich Klakow)
  • Aymeric Bouzy (MSc intern, implementation of corecursion up-to; cosupervisor: Dmitriy Traytel)
  • Simon Cruanes (postdoctoral software engineer, counterexample generation)
  • Martin Desharnais (BEng intern, properties of (co)datatypes; cosupervisor: Dmitriy Traytel)
  • Michaël Noël Divo (MSc, formalization of λ-calculi)
  • Daniel El Ouraoui (MSc intern, towards higher-order SMT; main supervisor: Pascal Fontaine)
  • Mathias Fleury (MSc intern, integration of provers in Sledgehammer and formalization of ground inference systems; cosupervisor: Dmitriy Traytel)
  • Charles Francis (Google Summer of Code, proof redirection)
  • Yuan Gao (BSc research assistant, genetic algorithms for time slicing)
  • Maximilian Haslbeck (MSc directed research, translation of Naproche to Isabelle; main supervisor: Tobias Nipkow)
  • Philipp Hermann (graduate research immersion lab, formalization of tableaux)
  • Hans-Dieter Hiep (MSc, generation of verification conditions for protocols; cosupervisor: Farhad Arbab)
  • 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)
  • Lorenz Panny (BSc, (co)recursive function definitions; cosupervisor: Dmitriy Traytel)
  • Anders Schlichtkrull (PhD, formalization of logical calculi; main supervisor: Jørgen Villadsen)
  • Anders Schlichtkrull (MSc, formalization of resolution; main supervisor: Jørgen Villadsen)
  • Steffen Juilf Smolka (BSc, structured Isabelle proofs from refutation proofs)
  • Albert Steckermeier (BSc, enhanced integration of Waldmeister in Sledgehammer)
  • Dmytro Traytel (MSc, (co)datatype definitions; main supervisor: Andrei Popescu)
  • Petar Vukmirović (MSc, implementation of λ-free higher-order superposition; cosupervisor: Stephan Schulz)
  • Jens Wagemaker (BSc, formalization of mathematics in Lean; cosupervisors: Johannes Hölzl and Sander Dahmen)
  • Daniel Wand (PhD, extensions of superposition; main supervisor: Christoph Weidenbach)

Drafts

  • A verified prover based on ordered resolution
    Anders Schlichtkrull, J. C. B., and Dmitriy Traytel.
    Draft paper (PDF)

Journal Articles

  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, J. C. B., Mathias Fleury, and Pascal Fontaine. Accepted in Journal of Automated Reasoning.
    Preprint (PDF)
  • A formal proof of the expressiveness of deep learning
    Alexander Bentkamp, J. C. B., and Dietrich Klakow. Accepted in Journal of Automated Reasoning.
    Free PDFWeb sitePreprint (PDF)
  • A verified SAT solver framework with learn, forget, restart, and incrementality
    J. C. B., Mathias Fleury, Peter Lammich, and Christoph Weidenbach. Journal of Automated Reasoning 61(1–4), pp. 333–365, 2018.
    Free PDFWeb pagePostprint (PDF)
  • Introduction to Milestones in Interactive Theorem Proving
    Jeremy Avigad, J. C. B., Gerwin Klein, Lawrence Paulson, Andrei Popescu, and Gregor Snelting. Journal of Automated Reasoning 61(1–4), pp. 1–8, 2018.
    Web pagePostprint (PDF)
  • A decision procedure for (co)datatypes in SMT solvers
    Andrew Reynolds and J. C. B. Journal of Automated Reasoning 58(3), pp. 341–362, 2017.
    Free PDFWeb pagePostprint (PDF)
  • Soundness and completeness proofs by coinductive methods
    J. C. B., Andrei Popescu, and Dmitriy Traytel. Journal of Automated Reasoning 58(1), pp. 149–179, 2017.
    Free PDFWeb pagePostprint (PDF)
  • Encoding monomorphic and polymorphic types
    J. C. B., Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Logical Methods in Computer Science 12(4:13), 2016, pp. 1–52.
    Postprint (PDF)
  • A learning-based fact selector for Isabelle/HOL
    J. C. B., David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. Journal of Automated Reasoning 57(3), pp. 219–244, 2016.
    Free PDFWeb pagePostprint (PDF)
  • Semi-intelligible Isar proofs from machine-generated proofs
    J. C. B., Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. Journal of Automated Reasoning 56(2), pp. 155–200, 2016.
    Web pagePostprint (PDF)
  • Hammering towards QED
    J. C. B., Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Journal of Formalized Reasoning 9(1), pp. 101–148, 2016.
    Web pagePostprint (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 pagePostprint (PDF)
  • LEO-II 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 pagePostprint (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 pagePostprint (PDF)
  • Monotonicity inference for higher-order formulas
    J. C. B. and Alexander Krauss. Journal of Automated Reasoning 47(4), pp. 369–398, 2011.
    Web pagePostprint (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 pagePostprint (PDF)

Conference Papers

  • Bindings as bounded natural functors
    J. C. B., Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Accepted at 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).
    Preprint (PDF)Report (PDF)
  • Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited paper)
    J. C. B. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019).
    Draft paper (PDF)
  • Superposition with datatypes and codatatypes
    J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • Superposition for lambda-free higher-order logic
    Alexander Bentkamp, J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • Formalizing Bachmair and Ganzinger's ordered resolution prover
    Anders Schlichtkrull, J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • A verified SAT solver with watched literals using Imperative HOL
    Mathias Fleury, J. C. B., 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
    J. C. B., 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—Leibniz-Zentrum für Informatik, 2017.
    Postprint (PDF)
  • A formal proof of the expressiveness of deep learning
    Alexander Bentkamp, J. C. B., and Dietrich Klakow. In Ayala-Rincón, M., Muños, C. A. (eds.) 8th Conference on Interactive Theorem Proving (ITP 2017), LNCS 10499, pp. 46–64, Springer, 2017.
    Web pagePostprint (PDF)
  • A verified SAT solver framework with learn, forget, restart, and incrementality
    J. C. B., Mathias Fleury, and Christoph Weidenbach. In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790, ijcai.org, 2017.
    Web pagePostprint (PDF)
  • Foundational (co)datatypes and (co)recursion for higher-order logic
    Julian Biendarra, J. C. B., 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 pagePostprint (PDF)
  • A transfinite Knuth–Bendix order for lambda-free higher-order terms
    Heiko Becker, J. C. B., Uwe Waldmann, and Daniel Wand. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 432–453, Springer, 2017.
    Web pagePostprint (PDF)Report (PDF)
  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, J. C. B., and Pascal Fontaine. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 398–412, Springer, 2017.
    Web pagePostprint (PDF)Report (PDF)
  • Foundational nonuniform (co)datatypes for higher-order logic
    J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • A lambda-free higher-order recursive path order
    J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • Friends with benefits: Implementing corecursion in foundational proof assistants
    J. C. B., 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 pagePostprint (PDF)Report (PDF)
  • A decision procedure for (co)datatypes in SMT solvers
    Andrew Reynolds and J. C. B. In Kambhampati, S. (ed.) 25th International Joint Conference on Artificial Intelligence (IJCAI-16), pp. 4205–4209, IJCAI/AAAI Press, 2016.
    Web pagePostprint (PDF)
  • A verified SAT solver framework with learn, forget, restart, and incrementality
    J. C. B., 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, J. C. B., 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
    J. C. B., 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 J. C. B. In Felty, A., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE-25), LNCS 9195, pp. 197–213, Springer, 2015.
    Postprint (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), LNCS 9150, pp. 1–15, Springer, 2015.
    Postprint (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.
    Postprint (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, 2014.
    Web pagePostprint (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 pagePostprint (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 pagePostprint (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), LNCS 8562, pp. 46–60, Springer, 2014.
    Web pagePostprint (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), LNCS 8152, pp. 245–260, Springer, 2013.
    Web pagePostprint (PDF)
  • MaSh: Machine learning for Sledgehammer
    Daniel Kühlwein, J. C. B., Cezary Kaliszyk, and Josef Urban. In Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th Conference on Interactive Theorem Proving (ITP 2013), LNCS 7998, pp. 35–50, Springer, 2013.
    Web pagePostprint (PDF)
  • TFF1: The TPTP typed first-order form with rank-1 polymorphism (system description)
    J. C. B. and Andrei Paskevich. In Bonacina, M. P. (ed.) 24th International Conference on Automated Deduction (CADE-24), LNCS 7898, pp. 414–420, Springer, 2013.
    Web pagePostprint (PDF)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 pagePostprint (PDF)
  • Foundational, compositional (co)datatypes for higher-order 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 Computer Society, 2012.
    Web pagePostprint (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 pagePostprint (PDF)
  • Automatic proof and disproof in Isabelle/HOL
    J. C. B., Lukas Bulwahn, and Tobias Nipkow. In Tinelli, C., Sofronie-Stokkermans, V. (eds.) 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), LNCS 6989, pp. 12–27, Springer, 2011.
    Web pagePostprint (PDF)
  • Extending Sledgehammer with SMT solvers
    J. C. B., Sascha Böhme, and Lawrence C. Paulson. In Bjørner, N., Sofronie-Stokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE-23), LNCS 6803, pp. 116–130, Springer, 2011.
    Web pagePostprint (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, 2011.
    Web pagePostprint (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), LNCS 6397, pp. 117–141, Springer, 2010.
    Web pagePostprint (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 pagePostprint (PDF)
  • Monotonicity inference for higher-order formulas
    J. C. B. 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 pagePostprint (PDF)
  • Nitpick: A counterexample generator for higher-order 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 pagePostprint (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 pagePostprint (PDF)
  • Nitpick: A counterexample generator for higher-order 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)Postprint (PDF)

Workshop Papers

  • Language and proofs for higher-order SMT (work in progress)
    Haniel Barbosa, J. C. B., 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 pagePostprint (PDF)
  • Extending Nunchaku to dependent type theory
    Simon Cruanes and J. C. B. Hammers for Type Theories (HaTT 2016)
    Postprint (PDF)
  • Model finding for recursive functions in SMT
    Andrew Reynolds, J. C. B., 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, J. C. B., and Dmitriy Traytel. Isabelle Workshop 2014.
    Postprint (PDF)
  • My life with an automatic theorem prover
    J. C. B. 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
    J. C. B. 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, semi-intelligible Isabelle proofs from ATP proofs
    Steffen Juilf Smolka and J. C. B. 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
    J. C. B. 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 J. C. B. 8th International Workshop on the Implementation of Logics (IWIL-2010).
    Full proceedings (PDF)Postprint (PDF)
  • Intra-object versus inter-object: 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 pagePostprint (PDF)
  • An open system operational semantics for an object-oriented and component-based 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 pagePostprint (PDF)

Workshop Abstracts

  • A verified SAT solver with watched literals using Imperative HOL (extended abstract)
    Mathias Fleury, J. C. B., and Peter Lammich. Isabelle Workshop 2018.
    Abstract (PDF)
  • Towards strong higher-order automation for fast interactive verification
    J. C. B., 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 pagePostprint (PDF)

  • An Isabelle formalization of the expressiveness of deep learning (extended abstract)
    Alexander Bentkamp, J. C. B., 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.
    Abstract (PDF)
  • Friends with benefits: Implementing foundational corecursion in Isabelle/HOL (extended abstract)
    J. C. B., Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Isabelle Workshop 2016.
    Abstract (PDF)
  • A verified SAT solver framework with learn, forget, restart, and incrementality (extended abstract)
    J. C. B., Mathias Fleury, and Christoph Weidenbach. Isabelle Workshop 2016.
    Abstract (PDF)
  • Model finding for recursive functions in SMT
    Andrew Reynolds, J. C. B., and Cesare Tinelli. QUANTIFY 2015.
    Abstract (PDF)
  • 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, presented at poster session.
    Abstract (PDF)

Theses

  • Automatic Proofs and Refutations for Higher-Order Logic
    J. C. B. PhD thesis, Fakultät für Informatik, Technische Universität München, June 2012.
    PDF
  • Verification of Assertions in Creol Programs
    J. C. B. MSc thesis, Institutt for informatikk, Universitetet i Oslo, May 2008.
    PDF

Books

  • Seventh International Conference on Interactive Theorem Proving (ITP 2016)
    J. C. B. and Stephan Merz (eds.)
    LNCS 9807, Springer, 2016.
    Web page
  • First International Workshop on Hammers for Type Theories (HaTT 2016)
    J. C. B. and Cezary Kaliszyk (eds.)
    EPTCS 210, 2016.
    Web pagePDF
  • Ninth International Conference on Tests and Proofs (TAP 2015)
    J. C. B. and Nikolai Kosmatov (eds.)
    LNCS 9154, Springer, 2015.
    Web page
  • Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013)
    J. C. B. and Josef Urban (eds.)
    EPiC 14, EasyChair, 2013.
    Web pagePDF
  • 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 pagePDF
  • 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 pagePDF

Other Publications

  • 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)
  • 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
  • Windows-to-Linux migration with Qt
    J. B. TUX 4, July 2005.
    Web page

Formal Proofs

  • Operations on bounded natural functors
    J. C. B., Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2018.
    Web page
  • Formalization of Bachmair and Ganzinger's ordered resolution prover
    Anders Schlichtkrull, J. C. B., Dmitriy Traytel, and Uwe Waldmann. Archive of Formal Proofs, 2018.
    Web page
  • Abstract soundness
    J. C. B., Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2017.
    Web page
  • Formalization of Knuth–Bendix orders for lambda-free higher-order terms
    Heiko Becker, J. C. B., Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016.
    Web page
  • Formalization of nested multisets, hereditary multisets, and syntactic ordinals
    J. C. B., Mathias Fleury, and Dmitriy Traytel. Archive of Formal Proofs, 2016.
    Web page
  • Formalization of recursive path orders for lambda-free higher-order terms
    J. C. B., Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016.
    Web page
  • Abstract completeness
    J. C. B., Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2014.
    Web page
  • Sound and complete sort encodings for first-order logic
    J. C. B. and Andrei Popescu. Archive of Formal Proofs, 2013.
    Web page
  • The textbook proof of Huffman's algorithm
    J. C. B. Archive of Formal Proofs, 2008.
    Web page

Software

  • Nunchaku—A stand-alone higher-order 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


Videos

  • Inria Inside—Jasmin Blanchette, 2016.
    YouTube
  • Qt 4 Dance, 2005. Jean-Claude, c'est moi.
    YouTube

Address

dr. J.C. Blanchette
W&N Building, Room T-437
Vrije Universiteit Amsterdam
Department of Computer Science
Section of Theoretical Computer Science
De Boelelaan 1081a
1081 HV Amsterdam
The Netherlands

Phone: +31 20 598 9886
Email: j.c.blanchette the at sign 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