If you made any changes in Pure these will be visible here soon.

Personal profile

Personal information

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 VeriDisgroup 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 (SledgehammerNitpickNunchaku, 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).


Ancillary activities

No ancillary activities

Ancillary activities are updated daily

Fingerprint Fingerprint is based on mining the text of the person's scientific documents to create an index of weighted terms, which defines the key subjects of each individual researcher.

  • 1 Similar Profiles
Data structures Engineering & Materials Science
Higher-order Logic Mathematics
Surface mount technology Engineering & Materials Science
Recursive functions Engineering & Materials Science
Superposition Mathematics
Functional programming Engineering & Materials Science
Syntactics Engineering & Materials Science
Calculus Mathematics

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 2016 2019

Scalable Fine-Grained Proofs for Formula Processing

Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., 1 Jan 2019, (Accepted/In press) In : Journal of Automated Reasoning.

Research output: Contribution to JournalArticleAcademicpeer-review

Surface mount technology
Data structures

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Blanchette, J. C., Fleury, M., Lammich, P. & Weidenbach, C., 12 Mar 2018, In : Journal of Automated Reasoning. 2018, p. 1-33 33 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Functional programming
Computer programming languages
Data structures

A verified SAT solver with watched literals using Imperative HOL

Fleury, M., Blanchette, J. C. & Lammich, P., Jan 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Data structures

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Schlichtkrull, A., Blanchette, J. C., Traytel, D. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 89-107 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI)

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Theorem proving
Automated Reasoning
Formal Proof
Theorem Proving

Introduction to Milestones in Interactive Theorem Proving

Avigad, J., Blanchette, J. C., Klein, G., Paulson, L., Popescu, A. & Snelting, G., Jun 2018, In : Journal of Automated Reasoning. 61, 1-4, p. 1-8 8 p.

Research output: Contribution to JournalEditorialAcademicpeer-review