Research output per year
Research output per year
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.
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
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
Network
Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
Research output
-
A modular isabelle framework for verifying saturation provers
Tourret, S. & Blanchette, J., Jan 2021, CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, Inc, p. 224-237 14 p.Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review
Open Access -
A Unifying Splitting Framework
Ebner, G., Blanchette, J. & Tourret, S., 2021, Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 344-360 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review
-
Functional Algorithms, Verified!
Nipkow, T., Blanchette, J. C., Eberl, M., Gómez-Londoño, A., Lammich, P., Sternagel, C., Wimmer, S. & Zhan, B., 2021Research output: Online publication or Non-textual form › Online publication or Website › Academic
-
Making Higher-Order Superposition Work
Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V. & Tourret, S., 2021, Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 415-432 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review
-
Message from the New Editor-in-Chief
Blanchette, J., Feb 2021, In: Journal of Automated Reasoning. 65, 2, p. 155-155 1 p.Research output: Contribution to Journal › Editorial › Academic › peer-review
Datasets
-
Superposition for Lambda-Free Higher-Order Logic — Supplementary Material
Bentkamp, A. (Contributor), Cruanes, S. (Contributor), Blanchette, J. C. (Contributor) & Waldmann, U. (Contributor), Unknown Publisher, 30 Jun 2018
DOI: 10.5281/zenodo.3975512, https://zenodo.org/record/3975512
Dataset