Rencontre, 9 mars 2017

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 low-level operational model for higher-order 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 lambda-calculus can relate to linear logic. In a second independent part, we shall recap what is a proof-net, and describe the two operational semantics on proof-nets 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 proof-nets, 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
• lambda-calculus
• linear logic
• (some) notion of linear algebra

14:00 – 15:00

Hugo Paquet (Cambridge)

Invited talk: Concurrent game semantics for Probabilistic PCF and relational collapse

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 lax-functorial, 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 real-valued, 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.