Here is the preliminary schedule for the workshop. Click on a talk to see its abstract.

**Samson Abramsky, "Big Toy Models"**

We pursue a model-oriented rather than axiomatic approach to the foundations of Quantum Mechanics, with the idea that new models can often suggest new axioms. This approach has often been fruitful in Logic and Theoretical Computer Science. Rather than seeking to construct a simplified toy model, we aim for a ‘big toy model’, in which both quantum and classical systems can be faithfully represented, as well as, possibly, more exotic kinds of systems. To this end, we show how Chu spaces can be used to represent physical systems of various kinds. In particular, we show how quantum systems can be represented as Chu spaces over the unit interval in such a way that the Chu morphisms correspond exactly to the physically meaningful symmetries of the systems --- the unitaries and antiunitaries. In this way we obtain a full and faithful functor from the groupoid of Hilbert spaces and their symmetries to Chu spaces. We also consider whether it is possible to use a finite value set rather than the unit interval; we show that three values suffice, while the two standard possibilistic reductions to two values both fail to preserve fullness.

**Jacob Biamonte, "The Computational Power of Minkowski Spacetime"**

View slides Link to paper

I will point out some properties of spacetime that allow an inertial classical computer to outperform a quantum one, at the completion of a journey. The comparison is between the optimal quadratic Grover speed up from quantum computing and an n=2 speedup using classical computers and relativistic effects. These results are not practical as a new model of computation, but allow us to probe the ultimate limits physics places on computation.

**Caslav Brukner, "Quantum Theory and Beyond: Is Entanglement Special?"**

View slides

Quantum theory makes the most accurate empirical predictions and yet it lacks simple, comprehensible physical principles from which the theory can be uniquely derived. A broad class of probabilistic theories exist which all share some features with quantum theory, such as probabilistic predictions for individual outcomes (indeterminism), the impossibility of information transfer faster than speed of light (no-signaling) or the impossibility of copying of unknown states (no-cloning). A vast majority of attempts to find physical principles behind quantum theory either fall short of deriving the theory uniquely from the principles or are based on abstract mathematical assumptions that require themselves a more conclusive physical motivation. Here, we show that classical probability theory and quantum theory can be reconstructed from three reasonable axioms: (1) (Information capacity) All systems with information carrying capacity of one bit are equivalent. (2) (Locality) The state of a composite system is completely determined by measurements on its subsystems. (3) (Reversibility) Between any two pure states there exists a reversible transformation. If one requires the transformation from the last axiom to be continuous, one separates quantum theory from the classical probabilistic one. A remarkable result following from our reconstruction is that no probability theory other than quantum theory can exhibit entanglement without contradicting one or more axioms.

**Earl T Campbell, "Bound States for Magic State Distillation"**

Magic state distillation is an important primitive in fault-tolerant quantum computation. The magic states are pure non-stabilizer states which can be distilled from certain mixed non-stabilizer states via Clifford group operations alone. Hence, any distillable non-stabilizer state is a resource for fault-tolerant quantum computation. Due to the Gottesman-Knill theorem, convex mixtures of Pauli eigenstates are not expected to be magic state distillable, but it has been an open question whether all mixed states outside this octahedral set may be distilled. I will outline our recent result showing that, when protocols are of finite size, non-distillable states exist outside the stabilizer octahedron. In analogy with the bound entangled states, which arise in entanglement theory, we call such states bound states for magic state distillation. References: Bound States for Magic State Distillation arXiv:0908.0836 On the Structure of Protocols for Magic State Distillation arXiv:0908.0838

**Bob Coecke, "Picturing Quantum and Classical Bayesian Inference"**

View slides

We provide categorical semantics and a corresponding purely diagrammatic presentation of Bayesian inference for probability distributions, as well as for a generalization of Bayesian inference to mixed quantum states. For this we rely on the graphical language of dagger symmetric monoidal categories, and of dagger Frobenius structures and compact structures. A paper is in preparation and should be ready at the time of the conference.

**Oscar Dahlsten, "All Reversible Dynamics in Maximally Non-Local Theories are Trivial"**

Link to paper

A remarkable feature of quantum theory is non-locality (i.e. the presence of correlations which violate Bell inequalities). However, quantum correlations are not maximally non-local, and it is natural to ask whether there are compelling reasons for rejecting theories in which stronger violations are possible. To shed light on this question, we consider post-quantum theories in which maximally non-local states (non-local boxes) occur. It has previously been conjectured that the set of dynamical transformations possible in such theories is severely limited. We settle the question affirmatively in the case of reversible dynamics, by completely characterizing all such transformations allowed in this setting. We find that the dynamical group is trivial, in the sense that it is generated solely by local operations and permutations of systems. In particular, no correlations can ever be created; non-local boxes cannot be prepared from product states (in other words, no analogues of entangling unitary operations exist), and classical computers can efficiently simulate all such processes.

**Tim Davidson, "Equivalence Relations for Communicating Quantum Processes"**

We present a probabilistic branching bisimilarity relation using the quantum process calculus Communicating Quantum Processes (CQP), which is a formal language for defining and reasoning about communicating quantum systems. Probabilistic branching bisimilarity is an example of behavioural equivalence, a concept that allows us to determine whether two systems act identically. We analyse a quantum teleportation protocol modelled in CQP and show that it is bisimilar to a process that performs no operations. The result of this is a statement of correctness of the teleportation model. We also present a congruence result for these processes and extend this to other processes that output qubits without changing their original state. This means that such statements of correctness can be applied when used in larger contexts.

**Alejandro Díaz-Caro, "A Vectorial System F"**

View slides Reference 1 Reference 2

This work is part of a program which seeks find a Quantum Physical Logic via the Curry-Howard correspondence applied upon a quantum programming language. As an intermediate aim we seek for a type system providing an understanding of normalisation and unitarity in a quantum setting. Indeed the linear-algebraic lambda-calculus (arXiv:quant-ph/0612199) extends the lambda-calculus with the ability to make arbitrary linear combinations of lambda-calculus terms, a.t+b.u. Terms can be understood as forming a vectorial space. Whilst this language has the potential for inducing novel forms of "vectorial" logics, dealing with concepts such as orthogonality and unitarity is not so trivial. We present three type systems. The scalar type system (arXiv:0903.3741) is a System F-like type system with scalars in the types. The additive type system is a type system with sums of types on it, which can be seen as a subset of the intuitionistic-multiplicative-exponential linear logic (IMELL). Combining these we develop a vectorial type system, which we believe will allow orthogonality checking between terms, via a notion of inner product of types. This talk will briefly cover these type systems, with emphasis on the vectorial type system, and discuss our ongoing work addressing the orthogonality issue.

**Andreas Doering, "Quantum States as Measures on the Spectral Presheaf"**

View slides Reference 1 Reference 2 Reference 3

States of a physical system -- classical or quantum -- can be seen as positive linear functionals of norm 1 (i.e., integrals) on the algebra of physical quantities. In classical physics, where the algebra is abelian, states are equivalently described by measures on the state space. A quantum system has a nonabelian algebra of physical quantities, and there is no obvious notion of a state space. We will show how quantum states can also be understood as measures, but now defined on a certain presheaf, called the spectral presheaf, which takes the role of the state space of the quantum system. The spectral presheaf is a central object in the topos approach to quantum theory. It will be shown how the spectral presheaf is related to, but different from the Gel'fand spectrum of a certain topos-internal operator algebra.

**Simon Gay, "Short Announcement"**

A short announcement about the QNET network

**Alexander S Green, "Formal Verification of the Quantum IO Monad"**

View slides Link to thesis

We have previously presented the Quantum IO monad (QIO), an interface to quantum programming from the functional programming language Haskell. This talk will present a new implementation of QIO, in the dependently typed programming language Agda. We can now use the stronger type system to give a formal verification of our semantics, in the sense that they contain proofs that the operators that can be defined are indeed unitary.

**Peter Hines, "A Tale of Two Programming Styles: Comparing Quantum & Classical Approaches to the Same Problem"**

View slides

This talk compares how quantum and classical computational paradigms are used to analyse and solve a simple problem (or class of problems). Classically, we consider algebraic, domain-theoretic, and categorical analyses. By contrast, in the quantum-mechanical setting we use the circuit paradigm in a very categorical setting. The intention is not to demonstrate an absolute advantage of one approach over the other, in terms of complexity classes; rather, we wish to compare & contrast two very different approaches to the same problem, in the hope of finding some common ground in the underlying theory.

**Matty Hoban, "Multi-Partite Computational Bell Inequalities"**

We show that all multi-partite Bell inequalities with two dichotomic observables per site are computational inequalities, that is, they can be expressed as bounds on the mean success probability of a distributed computational task in one time-step. We can then use tools such as variational methods and semi-definite programming to find the upper bound for quantum mechanics. The connection between the PR non-local box and the CHSH inequality is well established. We generalise the CHSH inequality to a multi-partite non-linear monomial function on more than two inputs. The quantum upper bound in this case does not exceed the classical upper bound. However, one can generalize the GHZ correlations to the multi-partite setting to then perform the task deterministically. These results illustrate a close connection between multi-partite Bell inequalities and measurement-based quantum computation, and inspire generalisations of the Bell inequality paradigm incorporating adaptive measurements, which should reveal further distinctions between quantum and classical correlations.

**Adrian Kent, "One World Versus Many: the Problems of Probability and Prediction""**

Link to paper

The idea that quantum theory describes many parallel worlds, first proposed by Everett in 1957, appeals to many theorists, and is often suggested as a way of understanding the power of quantum computing. However, even after fifty years, there is no consensus on what many-worlds quantum theory really means. For example, to many, it remains a mystery how we could make sense of probability, or replace it by something that plays an analogous role, in many worlds quantum theory. It is sometimes suggested that many worlds quantum theory is, at least, no worse off in this respect than standard probabilistic physical theories, where -- it is argued -- the meaning of probability turns out, under close examination, to be equally mysterious. In this talk, I counter this by pointing out a fundamental distinction between one-world and many-worlds theories: the former can be reframed in the language of algorithmic compressibility; the latter can't. This allows us to derive unambiguous and usefully testable experimental predictions from one-world theories -- something which, despite many ingenious attempts, we do not understand how to do, and which may in fact not be possible, in the case of many-worlds theories.

**Vladimir Kisil, "Turing Type Test for Quantum Computers and von Neumann Theorem"**

View slides

Assume that we are presented with a black box, which is claimed to be a quantum computer. Is it possible to confirm or disprove the claim if there are only classical devices in our disposal? Is there an analog of the famous Turing test for this purpose? We discuss this topic and its connections with the von Neumann theorem on composite systems.

**Aleks Kissinger, "Interacting Frobenius Algebras and the Structure of Multipartite Entanglement"**

We aim to present a structural scheme for representing arbitrary multipartite entangled states, in order to better understand how they behave and interact within quantum computational models and protocols. First we show that both the GHZ state and the W state admit a similar algebraic structure, which is only different in one important detail, and that for symmetric tripartite states this algebraic structure exactly characterises the corresponding SLOCC-entanglement classes. The interaction of these two algebraic structures yields a diagrammatic calculus that re-captures many of the behavioural properties of a large variety of multipartite entangled states. We illustrate some of these emergent properties and show how they inform an inductive technique for constructing arbitrary n-qubit states. References: Bound States for Magic State Distillation arXiv:0908.0836 On the Structure of Protocols for Magic State Distillation arXiv:0908.0838

**Neil Lovett, "Universal Quantum Computation Using the Discrete-Time Quantum Walk"**

View slides

The idea of using quantum walks for universal quantum computation has recently been investigated by Childs [PRL 102 180501 (2009)] using the continuous time quantum walk. We present an alternative form based instead on the discrete time quantum walk. We show the discrete time quantum walk can also be shown to be a computational primitive and are able to implement the same universal gate set.

**Nick Papanikolaou, "Automated Search for Quantum Secret Sharing Protocols"**

View slides

In this talk I will present work in progress on developing methods for finding graph-based quantum secret sharing protocols for graph states of varying dimensions. This builds on earlier work on verification of quantum protocols, but involves the development of new search algorithms and clever heuristics. This is joint work with Simon Gay (University of Glasgow).

**Dusko Pavlovic, "On the Measurement Problem in Categorical Semantics of Quantum Computation"**

In quantum computation, classical data are represented using the basis vectors, or more abstractly using classical structures. In the former case, the state collapse under measurement is captured using spectral decomposition. In the latter case, it corresponds to certain coalgebras derived from classical structures. In this talk, I shall review how we derive these measurement coalgebras, and discuss the measurement problem in this framework.

**Simon Perdrix, "Rewriting Measurement-Based Quantum Computations with Generalised Flow"**

View slides

We present a method for verifying measurement-based quantum computations, by producing a quantum circuit equivalent to a given deterministic measurement pattern. We define a diagrammatic presentation of the pattern, and produce a circuit via a rewriting strategy based on the generalised flow of the pattern. Unlike other methods for translating measurement patterns with generalised flow to circuits, this method uses neither ancilla qubits nor acausal loops. In addition this method can detect errors in the correction strategy used to make the pattern deterministic.

**Mehrnoosh Sadrzadeh, "What is the Vector Space Content of What We Say? A Quantum Informatic Approach to Meaning in Natural Languages"**

View slides

The two antipode approaches to semantics of natural languages are the symbolic and the distributed models of meaning. The former is type-logical and compositional, but does not say anything about meaning of words. The latter provides vector space meaning for words (based on their contexts), but says nothing about meaning of sentences. Developing a compositional distributed model of meaning has been a challenge to the computational linguists. Building on a proposal by linguists Clark and Pulman (Cambridge and Oxford), we merge these two approaches by using the axiomatics of compact closed categories and their diagrammatic toolkit of proofs. The key to this solution is our choice of Lambek's Pregroups as a syntax calculus, and the fact that both a Pregroup seen as a posetal category and the category of finite dimensional vector spaces are compact closed. We compute the meaning of a sentence by pre-composing the tensor product of the vectors of the words therein with the map of its syntactic structure. The pre-composition is a prescription on how to apply the units and counits of the adjunctions of the compact closed category. Surprisingly enough, the categorical Quantum Mechanics language of Abramsky and Coecke (Oxford) provides a nice intuitive explanation for the application of these maps: they create entangled Bell states (function abstraction) and take inner products (function application) and as such allow the information to flow among the words within a sentence. The use of two or more Bell states in the meaning map of negative sentences resembles the entanglement swapping protocols of quantum information.

**Apostol Vourdas, "Symplectic Transformations and Quantum Tomography in Finite Quantum Systems"**

View slides

Quantum systems where the position and momentum are in the ring Zd (d is an odd integer), are considered. Symplectic transformations are studied and the order of Sp(2, Zd) is shown to be dJ2(d), where J2(d) is the Jordan totient function. Quantum tomography is also discussed. It is shown that measurements (used in the inverse Radon transform) need to be made on at most J2(d) lines.