Categorical quantum mechanics

Categorical quantum mechanics is the study of quantum foundations and quantum information using paradigms from mathematics and computer science, notably monoidal category theory. The primitive objects of study are physical processes, and the different ways that these can be composed. It was pioneered in 2004 by Samson Abramsky and Bob Coecke.
Mathematical setup.
Mathematically, the basic setup is captured by a dagger symmetric monoidal category: composition of morphisms models sequential composition of processes, and the tensor product describes parallel composition of processes. The role of the dagger is to assign to each state a corresponding test. These can then be adorned with more structure to study various aspects. For instance:
A substantial portion of the mathematical backbone to this approach is drawn from Australian category theory, most notably from work by Max Kelly and M. L. Laplaza, Andre Joyal and Ross Street, A. Carboni and R. F. C. Walters, and 
Steve Lack.
Modern textbooks include C"ategories for quantum theory" and "Picturing quantum processes".
Diagrammatic calculus.
One of the most notable features of categorical quantum mechanics is that the compositional structure can be faithfully captured by a purely diagrammatic calculus.
These diagrammatic languages can be traced back to Penrose graphical notation, developed in the early 1970s. Diagrammatic reasoning has been used before in quantum information science in the quantum circuit model, however, in categorical quantum mechanics primitive gates like the CNOT-gate arise as composites of more basic algebras, resulting in a much more compact calculus. In particular, the ZX-calculus has sprung forth from categorical quantum mechanics as a diagrammatic counterpart to conventional linear algebraic reasoning about quantum gates. The ZX-calculus consists of a set of generators representing the common Pauli quantum gates and the Hadamard gate equipped with a set of graphical rewrite rules governing their interaction. Although a standard set of rewrite rules has not yet been established, some versions have been proven to be "complete", meaning that any equation that holds between two quantum circuits represented as diagrams can be proven using the rewrite rules. The ZX-calculus has been used to study for instance measurement based quantum computing.
Branches of activity.
Axiomatization and new models.
One of the main successes of the categorical quantum mechanics research program is that from seemingly weak abstract constraints on the compositional structure, it turned out to be possible to derive many quantum mechanical phenomena. In contrast to earlier axiomatic approaches, which aimed to reconstruct Hilbert space quantum theory from reasonable assumptions, this attitude of not aiming for a complete axiomatization may lead to new interesting models that describe quantum phenomena, which could be of use when crafting future theories.
Completeness and representation results.
There are several theorems relating the abstract setting of categorical quantum mechanics to traditional settings for quantum mechanics.
Categorical quantum mechanics as logic.
Categorical quantum mechanics can also be seen as a type theoretic form of quantum logic that, in contrast to traditional quantum logic, supports formal deductive reasoning. There exists software that supports and automates this reasoning.
There is another connection between categorical quantum mechanics and quantum logic, as subobjects in dagger kernel categories and dagger complemented biproduct categories form orthomodular lattices. In fact, the former setting allows logical quantifiers, the existence of which was never satisfactorily addressed in traditional quantum logic.
Categorical quantum mechanics as foundation for quantum mechanics.
Categorical quantum mechanics allows a description of more general theories than quantum theory. This enables one to study which features single out quantum theory in contrast to other non-physical theories, hopefully providing some insight into the nature of quantum theory. For example, the framework allows a succinct compositional description of Spekkens' toy theory that allows one to pinpoint which structural ingredient causes it to be different from quantum theory.
Categorical quantum mechanics as categorical compositional distributional semantics.
There have been attempts to build grammars using categorical quantum mechanics: a quantum process can be perceived as a sentence where the main function acts as the verb and takes the subject as an input and the object as an output. 
A main open problem with categorical compositional distributional semantics is the representation of words that do not carry meaning of their own from a distributional perspective, such as determiners, prepositions, relative pronouns, coordinators, etc. 