Dr. Jasmin Christian Blanchette
Senior Guest Researcher
Max-Planck-Institut für Informatik
Campus E1 4, Building E1 5, Room 621
Physical Address: Building E1 5, room 621
Phone: +49 (0)681 9325 2915
Fax: +49 (0)681 9325 2999
Home page: people.mpi-inf.mpg.de/~jblanche
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.