Preuves & Langages : Un Manège Enchanté

The Plume team belongs to the fundamental computer science [informatique fondamentale] theme of the FIL.

The research carried out by the members of the Plume team is mostly centered on two strongly intertwined themes: logical foundations of programming languages and theory of computing systems. International conferences announcing novel results in these areas include LICS, ICALP, POPL, CONCUR, CSL, FoSSaCS and ESOP.

Logical Foundations of Programming Languages

How can logic help in designing languages for writing safe programs?  We investigate proof theory as a foundation for programming languages and their semantics. In this area the proofs-as-programs correspondence has triggered the design of types systems, for statically ensuring properties, and of proof assistants for verifying correctness. Linear logic and game semantics are fundamental tools in this line of work and are themselves objects of current research. Some examples of challenges include: the definition of game semantics for concurrent languages conveniently crafted to overcome combinatorial explosion problems and the design of type systems that statically ensure complexity bounds on programs.

Theory of Computing Systems

How can one specify and formally verify complex computing systems?  We analyse computing systems using tools from logic, automata theory and category theory. In particular, we work on concurrent systems for which we try to develop co-inductive verification methods, based on operational semantics, as well as the mechanization of reasoning with these techniques. Concurrency and category theory have also been an inspiration for rule-based modeling, a programming paradigm for the representation and analysis of complex systems, in particular in biology. We also work on theoretical tools for verification: logics, games and algebraic systems. Monadic second-order logic (MSO) is studied from various viewpoints: using model-theoretic as well as proof-theoretic methods and by exploring topological and probabilistic aspects. Game semantics is applied in order to develop compositional approaches to model-checking. Algebraic systems for verification, such as Kleene algebras with tests (KAT) and their extensions, are explored for axiomatisations, decidability issues and mechanization through the Coq proof-assistant.