Multiple PhD and Postdoc Positions at LMU München about Automation of Higher-Order Logic

We are looking for PhD students (4 years) and postdoctoral researchers (3 years) who will work at the Ludwig-Maximilians-Universität in Munich, Germany. They will be hosted by the Chair of Theoretical Computer Science and Theorem Proving led by Prof. Jasmin Blanchette. The work will be supervised by Blanchette together with external experts and will be funded by the ERC project Nekoka.

Proof assistants (also called interactive theorem provers) have a long history of being very tedious to use. The situation has improved markedly in the past 10–15 years with the integration of first-order automatic theorem provers that increase proof automation. And recently, there have been exciting developments for more expressive logics, with the emergence of automatic provers based on optimized higher-order proof calculi. The Nekoka project’s aim is to make two of these calculi, higher-order SMT and lambda-superposition, a great fit for logical problems emerging from the verification of software and mathematics.

Nekoka is the logical successor of the Matryoshka project, which led to the development of lambda-superposition and its implementation in the E and Zipperposition provers. The Nekoka topics range from extending higher-order SMT and lambda-superposition to integrating them in general-purpose proof assistants (e.g., Isabelle, Lean) and software verification platforms (e.g., F*, TLA+ Proof System) to using the resulting automation in case studies related to quantum information theory and a big data framework.

For the postdoc positions, we are also interested in applicants who have their own research agenda compatible with the general aims of Nekoka.

The positions are categorized as TV-L E13 according to the German salary scale. The starting date is flexible. Please contact Jasmin Blanchette (jasmin dot blanchette at ifi dot lmu dot de) for more information or if you want to apply. Applications should include

1. a CV;
2. university transcripts;
3. a piece of text (e.g., a thesis or paper) you wrote yourself;
4. a piece of code or formalization you developed yourself;
5. the names and email addresses of two references;
6. a one-page research statement describing your research interests.

There is no application deadline. Applications will be processed continuously until the positions are filled.