A new connective in natural deduction, and its application to quantum computing

ALEJANDRO DÍAZ-CARO; GILLES DOWEK

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2021 vol. 1281 p. 175 - 193

0302-9743

[BEST PAPER AWARD]We investigate an unsuspected connection between non harmonious logical connectives, such as Prior´s tonk, and quantum computing. We defend 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 ⊙ (read: "sup", for "superposition") and show that its proof language forms the core of a quantum programming language.=========NOTA: El volume es 12819, pero SIGEVA sólo admite 4 dígitos.