Research output per year
Research output per year
Personal profile
Personal information
I am an associate 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.
Research
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).
Grants
NWO Vidi 2017
Lean Forward: Usable Computer-Checked Proofs and Computations for Number Theorists
ERC Starting Grant 2016
Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation
Ancillary activities
No ancillary activities
Ancillary activities are updated daily
Expertise related to UN Sustainable Development Goals
In 2015, UN member states agreed to 17 global Sustainable Development Goals (SDGs) to end poverty, protect the planet and ensure prosperity for all. This person’s work contributes towards the following SDG(s):
Fingerprint
Dive into the research topics where Jasmin Christian Blanchette is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
- 1 Similar Profiles
Collaborations and top research areas from the last five years
Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
-
Mechanical Mathematicians
Bentkamp, A., Blanchette, J., Nummelin, V., Tourret, S., Vukmirović, P. & Waldmann, U., Apr 2023, In: Communications of the ACM. 66, 4, p. 80-90 11 p.Research output: Contribution to Journal › Review article › Academic › peer-review
-
Recurrence-Driven Summations in Automated Deduction
Nummelin, V., Blanchette, J. & Dahmen, S. R., 2023, Frontiers of Combining Systems: 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings. Sattler, U. & Suda, M. (eds.). Cham: Springer Science and Business Media Deutschland GmbH, p. 23-40 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14279 LNAI).Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review
Open Access -
SAT-Inspired Eliminations for Superposition
Vukmirović, P., Blanchette, J. & Heule, M. J. H., Jan 2023, In: ACM Transactions on Computational Logic. 24, 1, p. 1-25 25 p., 3565366.Research output: Contribution to Journal › Article › Academic › peer-review
-
Superposition for Higher-Order Logic
Bentkamp, A., Blanchette, J., Tourret, S. & Vukmirović, P., Mar 2023, In: Journal of Automated Reasoning. 67, 1, p. 1-54 54 p., 10.Research output: Contribution to Journal › Article › Academic › peer-review
-
Unifying Splitting
Ebner, G., Blanchette, J. & Tourret, S., Jun 2023, In: Journal of Automated Reasoning. 67, 2, p. 1-44 44 p., 16.Research output: Contribution to Journal › Article › Academic › peer-review
Open Access
Courses
Datasets
-
SAT-Inspired Eliminations for Superposition
Vukmirovic, P. (Creator), Blanchette, J. C. (Creator) & Heule, M. J. H. (Creator), Zenodo, 2021
DOI: 10.5281/zenodo.4695128, https://zenodo.org/record/4695128
Dataset
-
Superposition for Lambda-Free Higher-Order Logic — Supplementary Material
Bentkamp, A. (Contributor), Blanchette, J. C. (Contributor), Cruanes, S. (Contributor) & Waldmann, U. (Contributor), Zenodo, 2018
DOI: 10.5281/zenodo.3975512, https://zenodo.org/record/3975512
Dataset
-
Superposition with Lambdas - Evaluation Data
Bentkamp, A. (Creator), Blanchette, J. C. (Creator), Tourret, S. (Creator), Vukmirovic, P. (Creator) & Waldmann, U. (Creator), Zenodo, 2020
DOI: 10.5281/zenodo.4032970, https://zenodo.org/record/4032970
Dataset
-
Superposition for Full Higher-Order Logic
Bentkamp, A. (Creator), Blanchette, J. C. (Creator), Tourret, S. (Creator) & Vukmirovic, P. (Creator), Zenodo, 2021
DOI: 10.5281/zenodo.4534759, https://zenodo.org/record/4534759
Dataset
-
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic -- Evalution Data
Vukmirovivc, P. (Creator), Blanchette, J. C. (Creator), Schulz, S. (Creator) & Cruanes, S. (Creator), Zenodo, 2020
DOI: 10.5281/zenodo.4045452, https://zenodo.org/record/4045452
Dataset