Schreiber Quantum Language via Linear Homotopy Types

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

A mini-course that I will have given:

Based on:

[1] The Quantum Monadology [arXiv:2310.15735]

[2] Entanglement of Sections [arXiv:2309.07245]

[3] Quantum and Reality [arXiv:2311.11035]

Abstract. It is well-appreciated that (intuitionistic but otherwise) classical (functional, programming) language is essentially the internal logic to cartesian closed categories (of data types), in particular to (higher) toposes — and that epistemology and other modality expressing physical observations and effects are reflected by (idempotent) co/monads on these categories.

In the course we explore how this classical situation naturally extends to subsume quantum logic of quantum systems controlled and measured by classical observers:

Here doubly closed monoidal categories (of entangled quantum data types parameterized by classical data), such as higher tangent toposes, reflect in their linear slices the substructural (no-deleting/no-cloning) quantum coherence, while their base change co/monads between linear slices turn out to know everything about decoherent quantum measurement (wavefunction collapse), including the ancient Born rule as well as contemporary spider-fusion in ZX-calculus string diagrams.

For example, the infamous quantum measurement paradox resolves in the internal logic to the deferred measurement principle which obtains a rigorous proof as the Kleisli equivalence of the quantum necessity modality. Diligent choice of do-notation for these quantum modalities gives a pleasantly natural universal quantum language which should be admissibly embeddable in some form of linear homotopy type theory to serve as a certifiable quantum programming language (working title: “QS”).


Lecture notes:

  • [to appear here]


Related talks:




Last revised on January 29, 2025 at 10:00:54. See the history of this page for a list of all contributions to it.

EditDiscussPrevious revisionChanges from previous revisionHistory (2 revisions) Print Source