Proofs and algorithms is one of the poles of the LIX lab at École Polytechnique.

Software and hardware systems perform computations (systems that process, compute and perform) and deduction (systems that search, check or prove). The makers of those systems express their intent using various frameworks such as programming languages, specification languages, and logics. Correctness of systems is a crucial issue. It is often necessary to go further, and also to be able to guarantee efficiency of conceived solutions, which sometimes depends heavily on the used paradigm or model of computation, or of the model of the underlying system.

The pole “Proofs and algorithms” aims at developing and using mathematical principles to design better frameworks for efficient and correct computations and reasoning,

We focus on foundational approaches, from theories to applications: studying fundamental problems of programming and proof theory (foundations of proof theory, semantics, computability and complexity theory, models of computations, foundations of complexity analysis for functional and imperative programming), modeling and analysis of programs and systems (invariants, temporal properties, correctness guarantees), computability and complexity theory for randomized algorithms, analog models of computations and constraint solving. One privileged field of applications concerns analog and numerical systems.

The pole consists of the following teams:

We have a common seminar.