Jasmin Christian Blanchette

Jasmin Christian Blanchette is an Associate Professor in the Theoretical Computer Science section at Vrije Universiteit Amsterdam, Netherlands. He holds visiting researcher positions at Loria (VeriDis group, Nancy, France) and the Max-Planck-Institut für Informatik (Automation of Logic group, Saarbrücken, Germany). Previously, he was a postdoc and PhD student at Technische Universität München (Germany) and worked as a software engineer and documentation manager for Trolltech (now The Qt Company) in Oslo, Norway.

Education & Career:

• PhD in Computer Science, Technische Universität München (2008–2012)
• Postdoc at TU München (2012–2016)
• Software Engineering Experience: Trolltech (2000–2008)

Research Focus: His work centers on automated theorem proving in higher-order logic, including tools like Sledgehammer, Nitpick, and Nunchaku. He develops definitional mechanisms for (co)datatypes and formalizes results in automated reasoning (IsaFoL) and number theory (Lean Forward). Key areas include superposition calculus, formal verification, and foundational logic frameworks.

Grants:

• NWO Vidi 2017: "Lean Forward: Usable Computer-Checked Proofs for Number Theorists"
• ERC Starting Grant 2016: "Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation"

Advising & Collaborations: Supervised 3 PhD theses (names not listed). Collaborates with international groups and contributes to open-source theorem proving tools. Active in projects like Matryoshka and Lean Forward.

Labs/Teams: Member of VeriDis (Loria) and Automation of Logic (MPI-INF) groups, focusing on interdisciplinary automated reasoning and formal methods.