Preuves & Langages : Un Manège Enchanté

The Plume team participates in the fundamental computer science [informatique fondamentale] theme of the FIL. Our research focuses on foundations for correct software with the particularity of combining expertise in ‘a priori’ methods for correctness by construction and ‘a posteriori’ methods for correctness by verification rooted in a common mathematical structures pole.

We make extensive use of tools such as category theory, the Coq system and complexity theory with the aim of providing tools for specific application domains such as program extraction and synthesis, model checking and executable knowledge for biology as well as more generic applications to the design and development of programming languages and proof assistants.

International conferences announcing novel results in these areas include LICS, ICALP, POPL, CONCUR, CSL, STACS, ICGT and FoSSaCS.

By construction

Our research in methods for correctness by construction is deeply informed by the Curry-Howard isomorphism between proofs and programs as exemplified by the Coq system. We build type systems to provide static guarantees for important properties of programs such as termination, absence of run-time errors, resource consumption and complexity of program execution. We use semantics, in particular game semantics, to analyse and compare sequential and concurrent programming primitives. We construct machine-assisted formalizations of mathematical theories, such as the calculus of relations, in Coq in order to bring standard verification techniques into the realm of proof assistants.

By verification

Our research in methods for correctness by verification combines traditional verification techniques with more recent developments in co-induction and co-algebra. We extend the scope of specification logics, such as LTL, modal µ-calculus and MSO, to probabilistic settings and higher-order model checking. We develop efficient new automata algorithms for proving language equivalences using ‘bisimulation up to’ techniques originating from process calculus. We exploit causality in graph rewriting to extract signalling pathways from simulation traces of models derived from biological knowledge.