The course notes
Lecture 1: Classical Logic as a typing system
Lecture 2: Confluence?
Lecture 3: An introduction to classical realisability
Exam March 2016
Solutions to Part II of 2017 exam
Internship proposal by Patrick Baillot
Internship proposal by Pascal Fontaine:
Matryoshka 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 Ph.D. positions due to start in the next two years and mainly located in Nancy (in close interaction with Amsterdam and Saarbruecken). 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 (firstname.lastname@example.org) and Pascal Fontaine (email@example.com) for more information.