Scientific organizers: Patrick Baillot (LIPN), Thomas Ehrhard (IML and PPS) and Laurent Regnier (IML).
This course will be an introduction to some recent development in constructive algebra. This approach can be seen as an application of some basic results in proof theory, the main one being the completeness of cut-free provability. It can be seen also as a partial realisation of Hilbert's program in abstract algebra, and uses the idea of "replacing" an infinite ideal object by a syntactical one: a logical theory which describes this object. It has also close connection with formal topology: cut-elimination can be expressed as forcing/topological semantics over a formal space. We show how this approach, besides revealing the computational content implicit in some abstract arguments in algebra, can lead to new concepts, new simple proofs of classical theorems, but also to new results in algebra.
The slides of this lecture are available here.
More details on this lecture, as well as references and links to relevant documents and articles, can be found there.
This lecture will present logical approaches to ensure complexity bounds on lambda-calculus or functional programs, with a particular emphasis on polynomial time complexity.
This line of research can be traced back to work by Leivant on restrictions of system F, and by Girard who showed that controling the logical rules responsible for duplication in Linear logic proofs made it possible to tame the complexity of the associated programs: he obtained in this way a logical characterization of elementary complexity (ELL system) and of polynomial time complexity (LLL system). Later Lafont proposed another variant of Linear logic also characterizing polynomial time. This course will also present the typed lambda-calculi that have been designed from these systems.
Another approach is based on restrictions of the primitive recursion scheme that lead to characterizations of polynomial time functions as well as of other complexity classes. This line was developed by Bellantoni and Cook and by Leivant and Marion. Later Marion adapted these ideas to the setting of first-order rewriting systems and showed that new criteria, based on termination orderings and quasi-interpretations provided flexible techniques to control the complexity of a large class of programs.
Finally Hofmann designed a type system for a functional language based on a fragment of Linear logic and ensuring that the typed programs are non-size-increasing and can be run in polynomial time.
This course will try to stress and discuss the issue of algorithmic expressivity: even if various systems characterize polynomial time functions, it is desirable that the languages obtained are expressive enough so as to be able to write some standard algorithms.