Rencontre, May 9, 2019
Programme
 10:30 – 12:00

Radu Mardare (Aalborg University (DK))
Complex probabilistic/stochastic processes are of central importance in modern computing, representing new challenges in Engineering and Technology, both from theoretical and practical perspectives. They involve realvalued parameters (probabilities of transitions, distributions characterizing the residencetime in a state, etc.) to abstract missing information, model ignorance, uncertainty or inherent randomness. Advances in verification of probabilistic and realtime systems as well as the tremendous growth of applications in cyberphysical systems, machine learning, and planning under uncertainty testify to their importance. To develop dedicated probabilistic/stochastic programming languages or theories of systems, one needs to reconsider the foundations of computational theory, since the classic logical principles supporting it must be replaced with nonclassical (e.g., measuretheoretic) probabilistic principles. More concretely, identifying probabilistic processes with identical probabilistic behaviours, as the classic computability theory does, is too `exact' for most purposes. In applications, one instead needs to know whether two processes that may differ by a small amount in their realvalued parameters have sufficiently similar behaviours, or to study the behavioural divergenceconvergence of inequivalent probabilistic programs.
In this talk I will discuss two such nonstandard semantics: the metric semantics and the Booleanvalued semantics, with their advantages and limitations. And I will present some technical details and challenges emerging form the metric semantics.
Bibliography:
[1] R. Mardare, P. Panangaden, G. Plotkin. Quantitative Algebraic Reasoning, LICS 2016.
[2] R. Mardare, P. Panangaden, G. Plotkin. On the Axiomatizability of Quantitative Algebras, LICS 2017.
[3] G. Bacci, R. Mardare, P. Panangaden, G. Plotkin. An Algebraic Theory of Markov Processes, LICS 2018.
[4] G. Bacci, R. Furber, D. Kozen, R. Mardare, P. Panangaden, Dana Scott. BooleanValued Semantics for Stochastic LambdaCalculus, LICS 2018.
 14:00 – 15:00

Mathys Rennela (LIACS, Leiden University, NL)Invited talk: Operator algebras in categorical quantum foundations
In this talk, we will present an overview of our work on the use of operator algebras as categorical models for quantum programming languages. Starting from a mathematical connection between operator theory and domain theory, we will detail some of the categorical properties of operator algebras, which can be represented as categories of presheaves. We present a general categorical framework for the semantics of embedded quantum programming languages as instances of enriched category theory, and establish some connection with probabilistic models, and Bentonstyle linearnonlinear models.
We explain how W*algebras fit within this framework. In detail, the denotational semantics is described as follows: every program type is interpreted as a W*algebra and every program is interpreted as a normal completely positive subunital map. These operator algebras were introduced by von Neumann himself, and motivated by his study of quantum mechanics. The theory of operator algebras has found direct application in various fields such as quantum information theory and quantum field theory.
We identify some relevant categorical properties of W*algebras and show they form a suitable setting for the mathematical interpretation of a firstorder quantum programming language with inductive datatypes. Since qubits are easily representable in a W*algebra, the denotational semantics supports many features relevant to quantum programming languages. We finally consider applications to verification and categorical axiomatics for quantum computing.
 15:30 – 16:30

Daniela Petrisan (IRIF, Univ. Paris Diderot)Invited talk: UpTo Techniques for Behavioural Metrics via Fibrations
Upto techniques are a wellknown method for enhancing coinductive proofs of behavioural equivalences. We introduce upto techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way.
In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of upto techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudometric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.