Menu

Home
People
Papers
Stages

Latest News

Meeting of July 17-18, 2013

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

Meeting of September 26, 2011

Meeting of June 23, 2011

Meeting of November 22, 2010

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.