Jasmin Blanchette

Jasmin Blanchette

Associate Professor

VU Theoretical Computer Science

I am an associate professor in Theoretical Computer Science at the Vrije Universiteit Amsterdam. I am also a guest researcher in the VeriDis group at Loria in Nancy, in the Automation of Logic group at the Max-Planck-Institut für Informatik in Saarbrücken, and in the Institut für Systemsicherheit of the Universität der Bundeswehr München. I did my PhD at the Chair for Logic and Verification at the Technische Universität München. Before that, I worked as software engineer and documentation manager for Trolltech (now The Qt Company) in Oslo.

Theorem proving plays a central role in formal methods and, more generally, in theoretical computer science. With my research, I work on strengthening proof automation for general-purpose logics and on making proof assistants more cost-effective to use. A hallmark of my research is the combination of automatic and interactive methods—of human and artificial intelligence. I envision a future in which automatic theorem provers and proof assistants will be routinely used for critical computing infrastructure, for programming language design, and more broadly for research in computer science and mathematics, thereby leading to more trustworthy systems and science.

Specifically, my research focuses on the development and use of automatic theorem provers and model finders to find proofs and counterexamples in higher-order logic (Sledgehammer, Nitpick, Nunchaku, and Matryoshka). I am also interested in formalizing classic results and modern research in automated reasoning (IsaFoL) and number theory (Lean Forward). Finally, I develop foundational definitional mechanisms for (co)datatypes and (co)recursive functions.

  • interactive and automatic theorem provers