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 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 (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