Rencontre, 9 mars 2017
La rencontre se tiendra en amphi B, à l'ENS de Lyon.
Programme
 10:30 – 12:00

Benoît Valiron (CentraleSupélec & LRI)Invited talk: A Geometry of Interaction for Quantum Computation
This tutorial will present a lowlevel operational model for higherorder quantum computation, using Geometry of Interaction as framework. The plan of the the session is a follows. In a first part, we shall see what is quantum computation, and how a suitably typed quantum lambdacalculus can relate to linear logic. In a second independent part, we shall recap what is a proofnet, and describe the two operational semantics on proofnets relevant to this talk: the first one using graph rewriting, the other using tokens flowing in the graph (aka what we call Geometry of Interaction). In the third and last part of the talk, we shall discuss how to merge the two constructions, to see how to get a quantum Geometry of Interaction. The construction is modular: we shall see how to add probabilistic behavior to proofnets, how to augment them with registers, and how to deal with the synchronization required for quantum computation. If time permits, we'll discuss an algebraic presentation of memory using nominal sets that is amenable to other computational models.
This presentation will assume basic knowledge of
 sequent calculus
 lambdacalculus
 linear logic
 (some) notion of linear algebra
 14:00 – 15:00

Hugo Paquet (Cambridge)
We introduce the concurrent game semantics of Probabilistic PCF (PPCF). The model consists of concurrent strategies based on event structures with symmetry, extending with probability a model of Castellan, Clairambault and Winskel.
We "collapse" this model to the weighted relational model of PPCF (Pagani et al), by forgetting the execution history of programs; we retain only the states reached by terminated executions. Usually such operations on strategies are only laxfunctorial, but we will see that terms of PPCF satisfy a condition called 'visibility', which ensures that no deadlock arise in their composition, and hence that the collapse to weighted relations is functorial.
Because probabilistic relations are fully abstract for PPCF, we obtain via the collapse that concurrent games are also (intensionally) fully abstract.
(Joint work with Simon Castellan, Pierre Clairambault & Glynn Winskel)
 15:30 – 16:30

Matteo Mio (CNRS, Lyon)Invited talk: Riesz Modal Logic for Markov Processes
We investigate a modal logic for expressing properties of Markov processes whose semantics is realvalued, rather than Boolean, and based on the mathematical theory of Riesz spaces. We use the duality theory of Riesz spaces to provide a connection between Markov processes and the logic. This takes the form of a duality between the category of coalgebras of the Radon monad (modeling Markov processes) and the category of a new class of algebras (algebraizing the logic) which we call modal Riesz spaces. As a result, we obtain a sound and complete axiomatization of the Riesz Modal logic.
This is joint work with Robert Furber and Radu Mardare.