Discrete Quantum Causal Dynamics We give a mathematical framework to describe the evolution of an open quantum systems subjected to finitely many interactions with classical apparatuses. The systems in question may be composed of distinct, spatially seperated subsystems which evolve independently but may also interact. This evolution, driven both by unitary operators and measurements, is coded in a precise mathematical structure in such a way that the crucial properties of causality, covariance and entanglement are faithfully represented. We show how our framework may be expressed using the language of (poly)categories and functors. Remarkably, important physical consequences - such as covariance - follow directly from the functoriality of our axioms. We establish strong links between the physical picture we propose and linear logic. Specifically we show that the refined logical connectives of linear logic can be used to describe the entanglements of subsystems in a precise way. Futhermore, we show that there is a precise correspondence between the evolution of a given system and deductions in a certain formal logical system based on the rules of linear logic.