CAPP - Calculi, Algorithms, Programs, and Proofs

At the heart of computer science lies the notion of computation, which can be modeled in many different ways. In addition to classical models of computation such as Turing machines, classical logic, or lambda-calculus, for which a lot remains to be explored, other non-classical models influenced by natural phenomena, noticed for instance in quantum physics or molecular biology, have attracted attention. Objects and processes from these fields have several interesting properties that can be used for encoding data, handling and transferring information or proving properties of computations.

Each model of computation leads to the design of specific theoretical tools intended to investigate their properties. Most of these investigations require the development of notations, languages, and other tools specifically tailored for the calculi themselves, their representations, for measuring the complexity, analyzing the behavior or verifying correctness of programs. They also lead to the development of hardware and software tools that implement or simulate these calculi, so that they can be applied to concrete problems, based on their specificities.

The CAPP team is a place where both classical and non-classical models of computation are designed and studied, with a focus on Calculi, Algorithms, Programs, and Proofs (CAPP).

The current topics of interests include: Graph Rewriting, Static Analysis, Reasoning in First-Order Logic with Equality, Separation logic, Hoare's logic, Quantum Computing, Inductive and abductive Reasoning.