Schreiber Quantum Certification via Linear Homotopy Types

Redirected from "Topological Quantum Programming in Linear Homotopy Type Theory".

A project that we are developing at CQTS:



The monadic aspect:


On the categorical semantics:


On the formalization of unitarity and dagger-structure:


The full picture, eventually to become a book (unfinished):



Brief survey:



Companion articles:




Expository presentations:



Related talks:


Precursor discussion:





Last revised on July 11, 2024 at 13:45:07. See the history of this page for a list of all contributions to it.