published (CUP) [ publisher ]
The unique features of the quantum world are explained in this book through the language of diagrams, setting out an innovative visual method for presenting complex theories. (more)
submitted [ arxiv ]
A systematic account of various metrics on probability distributions (states) and on predicates.
accepted (ESOP 2017) [ proceedings ]
We show that confluence is decidable for an extension of DPO rewriting to graphs with interfaces. (more)
published [ proceedings (LICS) · arXiv ]
We present a categorical construction for modelling both definite and indefinite causal structures within a general class of process theories that include classical probability theory and quantum theory. (more)
published [ proceedings (CALCO 2017) ]
We use companion functors to obtain an abstract GSOS-like extension result for specifications involving the second-order companion. (more)
submitted [ arXiv ]
We describe categorical models of a circuit-based (quantum) functional programming language. (more)
published [ proceedings (FSEN 2017) ]
Wc capture equivalence of open terms as bisimilarity on certain Mealy machines. (more)
published (EXPRESS/SOS 2017) [ arXiv ]
We show that monotone specifications - that disallow negative premises - do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional (more)
published (Journ. Math. Psych.) [ journal (JMP) ]
The paper demonstrates the usefulness of this effect logic in quantum cognition (more)
submitted [ arXiv ]
Disintegration and Bayesian inversion are explained in a categorical graphical language and with examples. (more)
published [ proceedings (MFCS 2017) ]
Influence is defined and to explain d-separation in Bayesian networks. (more)
published (MFCS 2017) [ preprint ]
Crossover influence is introduced and used to formalise d-separation in Bayesian networks. (more)
published (LMCS) [ arXiv ]
Normalisation and conditioning are reformulated as total `hyper’ operations. (more)
submitted [ arXiv ]
A mathematically precise definition of conjugate priors is given using channels. (more)
accepted [ arXiv ]
It is shown that quantum theory can be embedded into the category of quasi-probability distributions preserving convex, compositional and monoidal structure. (more)
published [ proceedings (CALCO TOOLS 2017) · preprint · EfProb ]
A brief overview is given of the possibilities of the EfProb library. (more)
published [ proceedings (MFPS) ]
We describe categorical models of a circuit-based (quantum) functional programming language. (more)
published [ proceedings (FoSSaCS 2017) · preprint (HAL) ]
We prove any causal function gives rise to a valid up-to-context technique. (more)
published [ journal (LMCS) ]
A basic construction to form state-and-effect triangles for program semantics is explained and illustrated. (more)
submitted [ proceedings (QPL) · arXiv ]
We give a new way to bound the security of QKD using only the diagrammatic behavior of complementary observables and essential uniqueness of purification for quantum channels. (more)
published [ journal (JLAMP) · preprint ]
A general theory of probabilistic monads is developed and related to commutative effectuses. (more)
published [ journal (LMCS) ]
We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples. (more)
published [ proceedings (MFPS 2016) · preprint ]
Bayesian inference is describe in terms of state and predicate transformation. (more)
published [ proceedings (MFPS 2016) · preprint ]
Properties of a monad are identified so that its Kleisli category is a commutative effectus. (more)
published [ journal (Information and Computation) ]
The basic theory of the expectation monad is developed. (more)
published [ preprint · proceedings (SPACE) ]
We explicitly construct oracles to solve binary MQ, which is the underlying hard problem of many proposed post-quantum cryptographic schemes.
published [ proceedings (CMCS 2016) · preprint ]
The notion of strongly affine monad is introduced and related to side-effect freeness of instruments which are associated with predicates. (more)
published [ proceedings (QPL) · arXiv ]
Following on from the notion of (first-order) causality, which generalises the notion of being tracepreserving from CP-maps to abstract processes, we give a characterization for the most general kind of map which sends causal processes to causal processes. (more)
published [ arXiv · proceedings (QPL) · video · slides ]
We generalize Stinespring to arbitrary completely positive normal maps between von Neumann algebra’s. (more)
published [ proceedings (QPL) ]
In this paper, W*-algebras are presented as canonical colimits of diagrams of matrix algebras and completely positive maps. In other words, matrix algebras are dense in W*-algebras.
published [ journal (JMP) ]
We study the sequential product, the operation on the set of effects of a von Neumann algebra that represents sequential measurement of first and then . We give four axioms which completely determine the sequential product.
published [ journal (QIC) · prequel ]
We study the notion of information cost in the quantum world. (more)
We interpret Selinger and Valiron’s quantum lambda calculus in the category of completely positive normal subunital maps between von Neumann algebras, and prove that the interpretation is adequate with respect to operational semantics.
published [ invited chapter · arXiv ]
This chapter uses categorical techniques to describe relations between various sets of operators on a Hilbert space, such as self-adjoint, positive, density, effect and projection operators. (more)
submitted [ preprint ]
In the present paper, convex dcpos are introduced as dcpos associated with a compatible convex structure. Convex dcpos are later used to adequately interpret PFPC, a probabilistic version of FPC, a functional programming language with recursive types.
done [ arXiv ]
Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. (more)
published [ invited chapter · arXiv ]
This chapter provides an introduction to the use of diagrammatic language, or perhaps more accurately, diagrammatic calculus, in quantum information and quantum foundations. (more)
accepted (TYPES 2015) [ arXiv ]
This paper introduces a novel type theory and logic for probabilistic reasoning. (more)
accepted (categories for the working philosopher) [ arXiv ]
We derive the category-theoretic backbone of quantum theory from a process ontology. (more)
published [ journal (EPTCS) ]
A uniform description is proposed for conditional probability which applies both the the classical and to the quantum case. (more)
published [ journal (LMCS) · arXiv ]
The basic theory of predicates as maps of the form \( X \rightarrow 1+1 \) and states of the form \( 1 \rightarrow X \), together with the duality between states and effects. This paper introduces a categorical description of instruments, which capture the side-effects associated with predicates (in the quantum case).
published [ proceedings (ICALP) · preprint ]
This paper starts with an effect algebraic approach to the study of non-locality and contextuality. (more)
published [ journal (LMCS) ]
We demonstrate a probabilistic version of Gelfand duality, involving the “Radon” monad on the category of compact Hausdorff space. (more)
published [ proceedings (QPL) · preprint · slides ]
The category of effectuses is equivalent to the category of FinPACs with effects, via the Kleisli construction for the lift monad (-)+1.
published [ proceedings (QPL) · preprint ]
A universal property for \( A \mapsto \sqrt{B} A \sqrt{B} \) appears in a chain of adjunctions.
published [ proceedings (MFPS) ]
We propose a new ‘quantum domain theory’ in which Scott-continuous functions are replaced by Scott-continuous natural transformations. (more)
published [ proceedings (MFPS) · preprint · slides ]
The step from probability measure to integral gets a universal property with the aid of ω-complete effect algebras and ω-complete effect modules.
published [ arXiv · proceedings (QPL) · preprint ]
The category of positive unital linear maps between C*-algebras is the Kleisli category of a comonad on the subcategory of unital *-homomorphisms between C*-algebras. (more)
published [ proceedings (POPL) · preprint ]
We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of quantum computing and quantum programming languages. We use the framework as follows: (more)
published [ proceedings (MFPS) ]
We discuss how the theory of operator algebras, also called operator theory, can be applied in quantum computer science. (more)
published [ proceedings (FoSSaCS) · preprint · slides ]
State spaces in probabilistic and quantum computation are convex sets, that is, Eilenberg–Moore algebras of the distribution monad. This article studies some computationally relevant properties of convex sets. (more)
published [ preprint · DOI · slides ]
We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs — effects on the appropriate Hilbert space. (more)
published [ proceedings (QPL) · preprint · arXiv · video · slides ]
The star-algebra \(M_2 \otimes M_2 \) models a pair of qubits. We show in detail that \(M_{3} \oplus \mathbb{C}\) models an unordered pair of qubits. Then we use the late 19th century Schur-Weyl duality, to characterize the star-algebra that models an unordered n-tuple of d-level quantum systems. (more)
published [ journal (NGC) · preprint · EPTCS · slides ]
A denotational semantics for Selinger’s first-order functional quantum programming language is given by W*-algebras and normal completely positive subunital maps.
published [ journal (NGC) · preprint · EPTCS · data · sourcecode · video · slides ]
A Kochen-Specker system has at least 22 vertices. (more)
done supervised by Bart Jacobs [ pdf ]
An investigation of the sequential product on predicates in the framework of Jacobs.
published [ proceedings (LICS) · preprint ]
Continuous probabilistic computation is shown to fit in the effect-theoretic framework. (more)