Menu

Home
People
Papers
Stages

Latest News

Meeting of July 17-18, 2013

• Damien Pous and Alan Schmitt: the KAM in HOcore
• Daniela Petrisan: Coalgebras over enriched categories. Slides
• Daniel Hirschkoff et Damien Pous: Bisimulations et bisimulations branchantes pour micro-ccs et micro-pi.
• Paul Brunet and Damien Pous: Equivalence of regular expressions with converse on relations. Slides
• Tom Hirschowitz: Un jeu pour le π calcul. Slides
• Clovis Eberhart: Towards a general construction of playgrounds. Slides
• Barbara Petit: Towards GCAB in Coq. Slides
• Sergueï Lenglet: Bisimulations for Delimited-Control Operators. Slides

Thomas Seiller's 68NQRT seminar (Rennes, June 13)

The Geometry of Interaction Program
This talk will be an introduction to the geometry of interaction program. Initiated by Jean-Yves Girard right after his discovery of Linear Logic, the program of Geometry of Interaction (GoI) aims at finding "semantics" of linear logic proofs that account for the dynamics of cut-elimination. Beyond the mere interpretation of proofs, it provides a complete reconstruction of logic around these dynamics. Looking at it through the glass of the proofs-as-programs correspondence, it is therefore a reconstruction of logic founded on the notion of execution, i.e. as the logic of (functional) programs. Several constructions have been proposed by Girard throughout the years, based on heavy mathematical tools (mainly operator algebras). Due to their execution-oriented foundations, they provide a natural and convenient framework for the study of complexity. Luckily for the audience, I showed that these constructions can be performed using only (for the main part) graph-theoretical notions. I will use these results to explain the main ideas behind this program and the known constructions that realize it.

Slides

Meeting of July 10, 2012

• Alan Schmitt: Formalisation de HOcore en Coq. papier, Transparents
• Jean-Marie Madiot: Duality and i/o-types in the pi calculus. transparents.

Meeting of September 26, 2011

• Tom Hirschowitz: Innocent strategies as presheaves and interactive equivalences for CCS (Joint with Damien Pous)

  Most of the audience already heard about our work on a game semantics for CCS. We will survey this work in the simplified form that it has taken in recent months, and present a few new results.

  1. The central piece of our approach is a category of (multi-player) plays, and its sub-categories of views and of closed-world plays, respectively. Strategies are defined as presheaves on views, and extend to (pre)sheaves on plays and on closed-world plays.
  2. Strategies enjoy two decomposition results, and we will sketch an efficient proof of temporal decomposition using weighted limits. Strategies are finally shown to be a final coalgebra for a certain polynomial functor on Set/N, the slice category of sets over natural numbers. This leads to a translation of an infinitary variant of CCS (including the more standard CCS with recursive definitions) into strategies.
  3. In a third part, we define our notion of interactive equivalence on strategies, and briefly explain the analogues of may, must, and fair testing in our framework. We finally sketch a proof that our translation of CCS preserves and reflects membership in the poles for may, must, and fair testing. That is, e.g., given a CCS process P, we have: any finite trace of P extends to a successful trace iff any state of the translation of P over a finite play extends to a successful state.

  Long version of the paper.

• Slides from Mateo Mio, The probabilistic modal μ-calculus with independent product

Meeting of June 23, 2011

• Slides from Enrico Tassi, Formal proofs and proof languages

Meeting of November 22, 2010

• Slides from Tom Hirschowitz, Fair testing vs. must testing in a fair setting
• Slides from Jean-Bernard Stefani, Components, Coalgebras, and Chu Spaces

The Project

The ubiquitous role played by software makes it necessary to analyze its properties in a rigorous manner, to state and prove guarantees about its behavior. However, an important part of modern software often consists in large distributed systems, with mobility or reconfiguration capabilities. By essence, such systems are almost impossible to analyze in a direct and global way: proofs on paper are not tractable, and automatic model-checking techniques are not expressive enough, or reach their limits because of state explosion.

Research in concurrency theory and process algebras has developed formal models for the description of many aspects of distributed programming. Abstract primitives have been proposed to model, at a foundational level, phenomena like distribution, higher-order communication, mobility, or component update. To some extent, behavioral theories have been built in order to state and prove properties of such systems, but work is needed to develop these into a corpus of powerful and actually usable proof techniques. Moreover, the need for rigorous guarantees justifies the use of formal methods, to certify the behavior of a given system. While writing computer-certified proofs has long been considered as an exercise involving "academic-size" proofs, recent work has confirmed that theorem provers are now mature enough to deal with large proofs, be it proofs of complex results in mathematics or proofs about programming language semantics (Gonthier and Werner's proof of the 4 color theorem, which required the development of sophisticated prover technology, or the certified compiler developed in the ANR project Compcert).

While the state of the art is rather advanced for sequential languages, tools for mechanical reasoning within a theorem prover about concurrent and distributed systems are currently missing. We propose in PiCoq to improve this situation by developing an environment for the formal verification of properties of distributed, component-based programs. Our approach lies at the interface between two research areas: concurrency theory and proof assistants. Achieving our goal relies on three scientific advances and a validation.

1. Find mathematical frameworks that ease modular reasoning about concurrent and distributed systems: due to their large size and complex interactions, distributed systems cannot be analyzed in a global way. They have to be decomposed into modular components, whose individual behavior can be understood.
2. Improve existing proof techniques for distributed/modular systems: while behavioral theories of first-order concurrent languages are well understood, this is not the case for higher-order ones. We also need to generalize well-known modular techniques that have been developed for first-order languages to facilitate formalization in a proof assistant, where source code redundancies should be avoided.
3. Define core calculi that both reflect concrete practice in distributed component programming and enjoy nice properties w.r.t. behavioral equivalences. This is closely related to point 2, as the proof techniques available for a given language strongly depend on the interaction of its primitives with behavioral equivalences. Beyond these theoretical advances, we expect the development of the proof environment itself to be quite challenging, as it will require several sophisticated proof-engineering techniques such as the handling of binders, implementation of tactics to solve automatically decidable statements, or smart usage of modules to make the code readable and reusable.
4. Finally, we will validate the developed tools by certifying some proofs about distributed component systems. Our validation will be threefold: formalize classic and recent articles about distributed systems, give a formal specification of a calculus that closely reflects a component model, and prove the correctness of a distributed abstract machine.