Curry-Howard correspondence for Classical Logic
MPRI

For any question, do not hesitate to write to Stephane.Lengrand[AT]Polytechnique.edu

The course notes

Lecture 1: Classical Logic as a typing system
Slides
Exercises

Lecture 2: Confluence?
Slides
Exercises A
Exercises B

Lecture 3: An introduction to classical realisability
Slides
Exercises correction

Exam March 2016
pdf

Solutions to Part II of 2017 exam

Internship proposal by Patrick Baillot

Internship proposal by Pascal Fontaine:

If you

interacting with the whole community of automated reasoning, this call is for you.

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 (jasmin.blanchette@inria.fr) and Pascal Fontaine (pascal.fontaine@inria.fr) for more information.