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.
- 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.
- 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.
- 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.
- 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 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.
- 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.
- 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.
- 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.
- 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.