Séminaire, 11 octobre 2012

Programme

10:30 – 12:00

Bernardo Toninho (Carnegie Mellon University)

Invited talk: Linear Logic: A logical foundation for concurrent computation

Linear logic has long been heralded as a potential model for concurrency: from Girard's original paper, to Abramsky's computational interpretation, reiterated by Bellin and Scott. More recently, an interpretation for intuitionistic linear logic has been given by Caires and Pfenning where propositions are viewed as session types - a well established typing discipline for concurrency - proofs as processes and proof reduction as inter-process communication. In this talk I will detail how this interpretation can form a basis to a logical foundation that captures several interesting features of concurrency and concurrent computation. Specifically, I will detail how one can capture concurrent evaluation strategies for functional computation through canonical logical translations; the relationship between isomorphisms in linear logic and (typed) process equivalence; how asynchronous communication can be interpreted logically and sketch how the interpretation can be extended to richer typed settings such as dependent type theories.

14:00 – 15:00

Thomas Seiller (LAMA - Université de Savoie)

Interaction Graphs

Geometry of Interaction (GoI) is a kind of semantics of linear logic proofs that aims at accounting for the dynamical aspects of cut-elimination. We present here a parametrized construction of a GoI for Multiplicative Additive Linear Logic (MALL) in which proofs are represented by families of directed weighted graphs. This construction is founded on a geometrical identity between sets of cycles which generalizes the three-term adjunctions which sustain usual GoI constructions. Moreover we show how one can obtain, for each value of the parameter, a denotational semantics for MALL from this GoI. Finally, we will explain how this setting is related to Girard's various constructions: two particular choices of the parameter respectively give a combinatorial version of the latest GoI in the hyperfinite factor and a refined version of older GoIs. Our construction hence shows how Girard's various constructions relate to each other by unveiling the unique geometrical identity sustaining them.

15:30 – 16:30

Christophe Raffalli (LAMA - Université de Savoie)

Realisability, call-by-value and Ramsey theorem

First, we will look at programs extracted from proofs of the infinite tape lemma (also called Stolzenberg's principle, which says that a partition of N in two has at least one infinite part). We will show how a specific axiom on streams allow the extraction of an efficient program.

Using this first program, we will extract programs for Ramsey theorem (not only for pairs) and as an application, we will get a program for the ``happy ending problem'' (for all N, in any infinite set of points, we can find N points which are the vertices of a convex polygon).

All those extracted programs are SML program using CallCC. To prove that those SML programs are indeed correct, we will introduce call-by-value realizability and see that it is a promising variation of classical realizability.