  We investigate an unsuspected connection between non harmonious logical
connectives, such as Prior's tonk, and quantum computing. We defend the idea
that non harmonious connectives model the information erasure, the
non-reversibility, and the non-determinism that occur, among other places, in
quantum measurement. More concretely, we introduce a propositional logic with a
non harmonious connective sup, prove cut elimination for this logic, and show
that its proof language forms the core of a quantum programming language.
