Séminaire, 15 mars 2012

Programme

10:30 – 12:00

Dale Miller (INRIA Saclay & LIX/Ecole Polytechnique)

Invited talk: Proof certificates as focused sequent proofs

Computational logic systems, such as theorem provers and model checkers, produce evidence of a successful proof in an assortment of (often ad hoc) formats. Unfortunately, the evidence generated by one prover is seldom readable by another prover or even by a future version of itself. As a result, provers seldom trust and use proofs from other provers. This situation is made all the more regrettable given that logic and (formal) proof are certainly candidates for universally accepted standards. I will outline some recent work on designing documents, called proof certificates, that satisfy the following requirements: (i) They are checkable by a simple proof checkers; (ii) They are flexible enough that existing provers can conveniently produce such certificates from their internal evidence of proof; (iii) They are directly related to proofs used within the structural proof theory literature; and (iv) They permit certificates to elide some proof information with the expectation that a proof checker can reconstruct the missing information using bounded and structured proof search. I shall show how the notion of focus sequent proofs can be used to design such proof certificates.

14:00 – 15:00

Nicolas Guenot (LIX/Ecole Polytechnique & PPS/Univ. Paris Diderot)

Nested typing and communication in the lambda-calculus

In a proof system based on the deep inference methodology (as implemented in the calculus of structures), new decompositions of inference steps appear and enrich the possible shapes of proofs. In particular, the lazy context splitting embodied in the "switch" rule is a distinctive feature of this methodology, which is related in an essential way to the order of inference steps used in a proof (which can often be seen as equivalent to a sequent proof, with a particular interleaving chosen for branches).

From a Curry-Howard perspective, we are interested in the computational meaning of such a decomposition. In this talk, I will present a system for intuitionistic logic in the calculus of structures, and show how to use it as a type system for a lambda-calculus with explicit substitutions. The switch rule, seen as a typing rule, introduces a new operator performing a synchronisation (that is, a form of communication) between different parts of a term. This yields interesting observations and questions, concerning communication between "subprocesses" of a term, evaluation strategies, the implementation of functional languages and the treatment of contexts.

15:30 – 16:30

Jean-Bernard Stefani (Sardes - INRIA Rhone-Alpes)

Invited talk: Reversing (HO)pi

The talk will present recent work dealing with the introduction of a notion of reversibility in concurrent languages. Reversibility refers to the ability to undo an execution and to revert it to a prior state. Such a facility can be useful for a variety of purposes, including debugging, safe exception handling, programming atomic operations and transactions, and more generally programming recoverable systems. The talk will discuss how to introduce reversibility in a paradigmatic concurrent language, the higher-order pi-calculus, and will discuss the subtleties involved in defining a semantically sound rollback primitive.