Skip to main content

CAPP - Calculi, Algorithms, Programs, and Proofs

Joint research team between CNRS, Grenoble INP, UGA
Area : Formal Methods, Models, and Languages

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.

Keywords

Programming Theory    Automated Theorem Proving    Program Verification    Rewriting Theory    Graph Transformation    Quantum computing    Superposition    Narrowing.

CAPP

Leader  Nicolas PELTIER
Website   http://capp.imag.fr
Phone  04 57 42 15 40
Building IMAG

Submitted on March 4, 2024

Updated on March 4, 2024