The CAPP team carries out research in theoretical computer science, especially in the fields of rewriting, logic, automated reasoning and quantum computing. We devise formalisms, algorithms and tools for the specification, design, analysis and certification of complex computing systems.
Motivations
Computing devices are more and more numerous, heterogeneous and complex and most human activity now depends on them. In this context, errors or malfunctions can have dramatic consequences, such as huge financial losses or human casualties, or more subtle issues such as wrong or inappropriate decisions. It is thus critical to make the development of these systems as easy and as rigorous as possible and to ensure that they behave in a proper way. It is also useful to equip computing devices with reasoning capabilities to make them able to extract explicit knowledge from the environment, to output convincing justifications to support their decisions, to interact with other agents etc. The CAPP team devises theoretical tools and results to help addressing these issues.
Research program
We design high-level languages to describe computations, suitable to various application domains and built on firm theoretical foundations, such as rewriting, logic or category theory. We investigate the properties of these models for the processing of information. We define logics to specify the properties of the computations and to establish their validity, and we investigate the expressivity and computability of these logics. We design automated reasoning procedures, implement them as research prototypes, and we apply these procedures to solve concrete problems. Reasoning is meant here in a very broad sense: we are interested not only in proving valid properties, but more generally in any task requiring deductive capabilities to extract knowledge, such as data analysis, synthesizing explanations or missing information, proof transformation etc.
A part of the team is interested in quantum computing, which has emerged as a key challenge at the border between computer science and physics. Quantum computing exploits quantum mechanics phenomena called superposition of states and entanglement to perform computations (e.g., a quantum bit may be in a state that is a superposition of 0 and 1, with some probabilities). These phenomena can be used to devise algorithms that run faster than any possible classical algorithm.