Several PhD Positions on Higher-Order Proof Automation at Inria Nancy, France

[Jørgen Villadsen]

If you

 

* want to pursue a PhD

* have a strong interest in logic

* want to understand how computers can do mathematical proofs

* want to contribute to the field in a very international environment interacting with the whole community of automated reasoning this call is for you.

Matryoshka (http://matryoshka.gforge.inria.fr/) is an ambitious research project that aims at developing efficient higher-order superposition provers and higher-order SMT (satisfiability modulo theories) solvers and integrating them in proof assistants. The project is funded by Jasmin Blanchette's European Research Council Starting Grant, from March 2017 to February 2022. It is co-located between Vrije Universiteit Amsterdam (Jasmin Blanchette) in the Netherlands and Inria Nancy – Grand Est (Pascal Fontaine) in France.

 

Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. To make interactive verification more cost-effective, we propose to deliver powerful automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. Our approach will be to enrich SMT and the superposition calculus with higher-order reasoning in a careful manner, to preserve their desirable properties. We will develop highly automatic provers building on modern SMT solvers and superposition provers, following a Russian doll architecture. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle/HOL, and the TLA+ Proof System.

 

We are looking for outstanding candidates for several funded PhD positions due to start in the next two years and mainly located in Nancy (in close interaction with Amsterdam and Saarbrücken). Candidates should ideally have some experience with automatic or interactive theorem proving and be at ease with both theory and engineering. Please contact Jasmin Blanchette (jasmin.b...@inria.fr) and Pascal Fontaine (pascal....@inria.fr) for more information.