Jasmin Christian Blanchette

I am a researcher in the VeriDis group at Inria Nancy – Grand-Est and LORIA in Nancy, France, and a senior guest researcher in the Automation of Logic group at the Max Planck Institute for Informatics in Saarbrücken, Germany. Until the end of 2014, 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 Ph.D. 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, and Nunchaku). 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).

See my home page for details.