Types for Quantum Computing

Quantum computation is a novel computational paradigm which makes use of entanglement - non-local correlations - to perform computations. From a mathematical point of view, a pair of entanged entangled systems may be viewed as a physical realistion of the linear function type - or more precisely as the PAR connective of multiplicative linear logic (MLL). In this talk I will examine the possibilities and limitations of linear logic as a typing regime for quantum processes, and how those limitations may be overcome using a generalised logical system based on polycategories.