Rencontre, 9 mai 2019

Programme

10:30 – 12:00
Radu Mardare (Aalborg University (DK))
Invited talk: Non-standard semantics for stochastic computational phenomena

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 real-valued parameters (probabilities of transitions, distributions characterizing the residence-time in a state, etc.) to abstract missing information, model ignorance, uncertainty or inherent randomness. Advances in verification of probabilistic and real-time systems as well as the tremendous growth of applications in cyber-physical 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 non-classical (e.g., measure-theoretic) 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 real-valued parameters have sufficiently similar behaviours, or to study the behavioural divergence-convergence of inequivalent probabilistic programs.

In this talk I will discuss two such non-standard semantics: the metric semantics and the Boolean-valued 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. Boolean-Valued Semantics for Stochastic Lambda-Calculus, 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 Benton-style linear-non-linear 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 first-order 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: Up-To Techniques for Behavioural Metrics via Fibrations

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to 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 up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.