Séminaire, 14 mars 2013
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Robin Cockett (University of Calgary)
Linear logic has since its inception been viewed as being closely connected to concurrency. However, making this connection explicit has been difficult as it lacked two key features of concurrent programs: the ability to pass messages and the ability to define protocols. Messages consist of data from the sequential world which can be passed along channels from one process to another, while protocols are types which describe patterns of interactions.
The talk will describe the semantics of these facilities in terms of a Curry-Howard-Lambek correspondence between the proof theory (the logic of message passing), the categorical semantics (linear categories), and the term logic (a concurrent programming language).
- 14:00 – 15:00
-
Chung-Kil Hur (Microsoft Research Cambridge)Invited talk: The Power of Parameterization in Coinductive Proof
In this talk, I will present a very simple principle for reasoning about coinduction, which we call parameterized coinduction. More precisely, it is a theorem about the greatest fixed point of a monotone function on a complete lattice. This theorem is as simple as the Tarski's fixed-point theorem but provides a more useful reasoning principle.
In a different point of view, the principle captures a semantic notion of "guarded proof" in coinduction. Thus we implemented a new tactic "pcofix" replacing Coq's primitive tactic "cofix" and avoiding its syntactic guardedness checking of proof terms.
You can find the Coq library 'Paco' that provides the tactic 'pcofix' at
This is joint work with Georg Neis, Derek Dreyer and Viktor Vafeiadis.
- 15:30 – 16:30
-
Emmanuel Beffara (Université d'Aix-Marseille)Invited talk: Proofs as schedules
This work proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to valid executions of a processes. A type system based on linear logic is used, in which a given process has many different types, each typing corresponding to a particular way of interacting with its environment and cut elimination corresponds to executing the process in a given interaction scenario. A completeness result is established, stating that every lock-avoiding execution of a process in some environment corresponds to a particular typing. Besides traces, types contain precise information about the flow of control between a process and its environment, and proofs are interpreted as composable schedulings of processes. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes.
Joint work with Virgile Mogbil.
