Research output per year
Research output per year
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.
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).
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
No ancillary activities
Ancillary activities are updated daily
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):
Research output: Contribution to Journal › Article › Academic › peer-review
Research output: Contribution to Journal › Review article › Academic › peer-review
Research output: Contribution to Journal › Article › Academic › peer-review
Research output: Contribution to Journal › Article › Academic › peer-review
Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review
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 / Software: Dataset
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 / Software: Dataset
Bentkamp, A. (Creator), Blanchette, J. C. (Creator), Cruanes, S. (Creator) & Waldmann, U. (Creator), Zenodo, 2020
DOI: 10.5281/zenodo.3992618, https://zenodo.org/record/3992618
Dataset / Software: Dataset
Blanchette, J. C. (Creator) & Vukmirović, P. (Creator), Zenodo, 2022
DOI: 10.5281/zenodo.6997515, https://zenodo.org/record/6997515
Dataset / Software: Dataset
Vukmirović, P. (Creator), Bentkamp, A. (Creator), Blanchette, J. C. (Creator), Cruanes, S. (Creator), Nummelin, V. (Creator) & Tourret, S. (Creator), Zenodo, 2021
DOI: 10.5281/zenodo.4534829, https://zenodo.org/record/4534829
Dataset / Software: Dataset