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.