Séminaire, 16 mai 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
-
Andrzej Murawski (University of Warwick)Invited talk: Deconstructing general references via game semantics
We investigate the game semantics of general references through the fully abstract game model of Abramsky, Honda and McCusker (AHM), which demonstrated that the visibility condition in games corresponds to the extra expressivity afforded by higher-order references with respect to integer references. First, we prove a stronger version of the visible factorisation result from AHM, by decomposing any strategy into a visible one and a single strategy corresponding to a reference cell of type unit -> unit (AHM accounted only for finite strategies and its result involved unboundedly many cells).
We show that the strengthened version of the theorem implies universality of the model and, consequently, we can rely upon it to provide semantic proofs of program transformation results. In particular, one can prove that any program with general references is equivalent to a purely functional program augmented with a single unit -> unit reference cell and a single integer cell. We also propose a syntactic method of achieving such a transformation. Finally, we provide a type-theoretic characterisation of terms in which the use of general references can be simulated with an integer reference cell or through purely functional computation, without any changes to the underlying types.
This is joint work with Nikos Tzevelekos (Queen Mary, University of London), presented at FOSSACS'13 earlier this year.
- 14:00 – 15:00
-
Jean-Marie Madiot (ENS Lyon)Invited talk: A pi-calculus with preorders
The fusion calculi are a simplification of the pi-calculus in which input and output are symmetric and restriction is the only binder. We highlight a major difference between these calculi and the pi-calculus from the point of view of types, proving some impossibility results for subtyping in fusion calculi. We propose a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. We examine the consequences of the modification on behavioural equivalence (e.g., context-free characterisations of barbed congruence) and expressiveness (e.g., full abstraction of the embedding of the asynchronous pi-calculus).
- 15:30 – 16:30
-
Alexandra Silva (Radboud University Nijmegen)
We give a brief introduction to the coalgebraic method and show two recent developments that attest its generality and usefulness.
We first show a new proof of Brzozowski's minimization algorithm and discuss generalizations resulting from this new perspective.
We then present CoCaml, a functional programming language extending OCaml, which allows us to define functions on coinductive datatypes parameterized by an equation solver. We provide compelling examples that attest to the usefulness of the new programming constructs.
