LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
Operator algebra-based models for quantum programming with inductive types (and beyond)
- Date
- 21.12.2020, 14:00
- Place
- online
- Speaker
- Mathys Rennela (Leiden Institute of Advanced Computer Science)
In this talk, we present an overview of our work on the use of operator algebras as categorical models for quantum programming languages. We put a particular focus on W*-algebras, a natural mathematical model used by physicists in the study of the foundations of quantum mechanics, with various applications in quantum information theory and quantum field theory. We present a general categorical framework for the semantics of embedded quantum programming languages as instances of enriched category theory. We establish some connections with probabilistic models, and Benton-style linear-non-linear models. We explain how W*-algebras fit within this framework, as a model for a first-order quantum programming language. Then, using W*-algebras, we define a denotational model of inductive datatypes, which include data structures for natural numbers, lists, trees, and so on. To exemplify this construction, we show how inductive types may be added to the quantum programming language QPL, and show that the resulting language admits a computationally adequate categorical model based on W*-algebras. We further cement the usefulness of W*-algebras (and more generally, operator algebras), through categorical constructions which highlight how W*-algebras arise in the study of (categorical) quantum foundations, and even probabilistic computing. We finally consider further applications of the theory of operator algebras to verification and categorical axiomatics for quantum computing.