Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2604.05671

A Global Model Structure for $\mathbb{K}$-Linear $\infty$-Local Systems

Hisham Sati, Urs Schreiber

math.ATmath.CTquant-phSubmitted Apr 7, 2026• Announced Apr 8, 2026
arXivHTMLPDF

Abstract

Parameterized stable homotopy theory organizes local systems of spectra over homotopy types, governed by a "yoga" of six functors. To provide semantics for the recently developed Linear Homotopy Type Theory (LHoTT), good model categories of these spectra are required, preferably monoidal with respect to the external smash product. We focus on the case of parameterized $H\mathbb{K}$-module spectra ($\infty$-local systems), motivated by recent applications of parameterized homotopy to topological quantum computing. While traditionally treated via dg-categories, we leverage combinatorial model structures on simplicial chain complexes to construct the first dedicated global model structure for $\mathbb{K}$-linear $\infty$-local systems, which offers better control than existing models for general parameterized spectra. In particular, when restricted to base 1-types, our model structure is monoidal with respect to the external tensor product, making it a candidate target semantics for the multiplicative fragment of LHoTT.

Comments
55 pages; the content of this article used to be the second half of arXiv:2309.07245v2, the first half of which has meanwhile been published separately

Related papers

Parameterized Quantum Circuit Semantics Through Enriched Categories

Neil J. Ross, Scott Wesley

It is well-known that combinatorial circuits are modeled mathematically by string diagrams in monoidal categories. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. In this paper, we introduce an approach to parameterized circuit semantics, which is based on enriched category theory. We first introduce an abstract categorical construction, and use this to gain new insights on controlled operations and quantum communication. We then study the special cases of Cartesian monoidal parameters and monoidal closed parameters, both endowing the parameterized semantics with useful constructions. We conclude by showing that the monoidal closed case can be used to unify two perspectives on quantum control.

quant-pharXiv:2607.16114•Jul 20, 2026•0 citations

Enriched Categories for Parameterized Circuit Semantics

Wesley, Scott

It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. Intuitively, this functor should be valued in parameterized families of unitary matices, though it is not immediately clear what this mean through a categorical lens. In this paper, we show that the parameterized semantics studied in prior work can be understood through enrichment and internal constructions. We determine sufficient conditions under which this construction yields a symmetric monoidal category, and suggest how these semantics could be extended to classical circuit analysis and parameterized equivalence checking.

arXiv:2501.12481•Jan 21, 2025•0 citations

Topological and geometrical quantum computation in cohesive Khovanov homotopy type theory

Juan Ospina

The recently proposed Cohesive Homotopy Type Theory is exploited as a formal foundation for central concepts in Topological and Geometrical Quantum Computation. Specifically the Cohesive Homotopy Type Theory provides a formal, logical approach to concepts like smoothness, cohomology and Khovanov homology; and such approach permits to clarify the quantum algorithms in the context of Topological and Geometrical Quantum Computation. In particular we consider the so-called “open-closed stringy topological quantum computer” which is a theoretical topological quantum computer that employs a system of open-closed strings whose worldsheets are open-closed cobordisms. The open-closed stringy topological computer is able to compute the Khovanov homology for tangles and for hence it is a universal quantum computer given than any quantum computation is reduced to an instance of computation of the Khovanov homology for tangles. The universal algebra in this case is the Frobenius Algebra and the possible open-closed stringy topological quantum computers are forming a symmetric monoidal category which is equivalent to the category of knowledgeable Frobenius algebras. Then the mathematical design of an open-closed stringy topological quantum computer is involved with computations and theorem proving for generalized Frobenius algebras. Such computations and theorem proving can be performed automatically using the Automated Theorem Provers with the TPTP language and the SMT-solver Z3 with the SMT-LIB language. Some examples of application of ATPs and SMT-solvers in the mathematical setup of an open-closed stringy topological quantum computer will be provided.

Proceedings of SPIE, the International Society for Optical Engineering/Proceedings of SPIE•May 21, 2015•0 citations

Categorified Spectral Duality: From Operator Systems to Spectral Stacks and Back

S. Chang

Classical Gelfand duality provides an equivalence between commutative C-star algebras and topological spaces, but fails to furnish a geometric object for noncommutative operator systems. To address this, we introduce a categorified notion of spectrum that captures the full operator-semantic structure. For an operator system A, we construct a spectral stack, denoted Spec(A), over the site of its commutative contexts. The construction proceeds in three stages. First, we encode the syntax of A via a colored operad called the synergy operad. Second, we aggregate local semantic data using a left Kan extension, providing an explicit coend formula. Third, we enforce descent via sheafification, yielding a stack that satisfies higher gluing conditions. We prove that Spec(A) satisfies a Yoneda-style universal property, making it the initial descent-complete semantic realization of A. This yields a contravariant functor from operator systems to spectral objects that admits a right adjoint, the global sections functor. Under semantic generation and descent completeness, the counit of this adjunction is an equivalence, establishing a reconstruction theorem: A is isomorphic to the endomorphisms of the structure sheaf on its spectrum. We further provide a recognition theorem characterizing the essential image of this functor and prove Morita invariance of the associated quasi-coherent sheaf categories. The construction naturally recovers classical Gelfand spectra and Bohrification as truncations of a Postnikov tower. Explicit computations for matrix algebras, Pauli systems, and the Mermin-Peres square yield a quantitative invariant of contextuality extracted from the inertia stack of Spec(A). Comparison theorems show that our framework subsumes Gelfand duality, Bohrification, and Tannaka reconstruction as special cases.

arXiv:2606.16949•Jun 15, 2026•0 citations

Linear Dependent Type Theory for Quantum Programming Languages

Peng Fu, Kohei Kishida, Peter Selinger

Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M in [28] constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.

ACM/IEEE Symposium on Logic in Computer Science (LICS)•May 26, 2020•22 citations

Linear Dependent Type Theory for Quantum Programming Languages

Peng Fu, Kohei Kishida, Peter Selinger

Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.

arXiv:2004.13472•Logical Methods in Computer Science•Sep 7, 2022•13 citations
A Global Model Structure for K\mathbb{K}K-Linear ∞\infty∞-Local Systems
Parameterized stable homotopy theory organizes local systems of spectra over homotopy types, governed by a "yoga" of six functors. To provide semantics for the recently developed Linear Homotopy Type Theory (LHoTT), good model categories of these spectra are required, preferably monoidal with respect to the external smash product.
We focus on the case of parameterized HKH\mathbb{K}HK-module spectra (∞\infty∞-local systems), motivated by recent applications of parameterized homotopy to topological quantum computing. While traditionally treated via dg-categories, we leverage combinatorial model structures on simplicial chain complexes to construct the first dedicated global model structure for K\mathbb{K}K-linear ∞\infty∞-local systems, which offers better control than existing models for general parameterized spectra. In particular, when restricted to base 1-types, our model structure is monoidal with respect to the external tensor product, making it a candidate target semantics for the multiplicative fragment of LHoTT.
It is well-known that combinatorial circuits are modeled mathematically by string diagrams in monoidal categories. Given a gate set ΣΣΣ, the circuits over ΣΣΣ can be thought of as string diagrams in the free monoidal category generated by ΣΣΣ. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. In this paper, we introduce an approach to parameterized circuit semantics, which is based on enriched category theory. We first introduce an abstract categorical construction, and use this to gain new insights on controlled operations and quantum communication. We then study the special cases of Cartesian monoidal parameters and monoidal closed parameters, both endowing the parameterized semantics with useful constructions. We conclude by showing that the monoidal closed case can be used to unify two perspectives on quantum control.
It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set ΣΣΣ, the circuits over ΣΣΣ can be thought of as string diagrams in the free monoidal category generated by ΣΣΣ. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. Intuitively, this functor should be valued in parameterized families of unitary matices, though it is not immediately clear what this mean through a categorical lens. In this paper, we show that the parameterized semantics studied in prior work can be understood through enrichment and internal constructions. We determine sufficient conditions under which this construction yields a symmetric monoidal category, and suggest how these semantics could be extended to classical circuit analysis and parameterized equivalence checking.
The recently proposed Cohesive Homotopy Type Theory is exploited as a formal foundation for central concepts in Topological and Geometrical Quantum Computation. Specifically the Cohesive Homotopy Type Theory provides a formal, logical approach to concepts like smoothness, cohomology and Khovanov homology; and such approach permits to clarify the quantum algorithms in the context of Topological and Geometrical Quantum Computation. In particular we consider the so-called “open-closed stringy topological quantum computer” which is a theoretical topological quantum computer that employs a system of open-closed strings whose worldsheets are open-closed cobordisms. The open-closed stringy topological computer is able to compute the Khovanov homology for tangles and for hence it is a universal quantum computer given than any quantum computation is reduced to an instance of computation of the Khovanov homology for tangles. The universal algebra in this case is the Frobenius Algebra and the possible open-closed stringy topological quantum computers are forming a symmetric monoidal category which is equivalent to the category of knowledgeable Frobenius algebras. Then the mathematical design of an open-closed stringy topological quantum computer is involved with computations and theorem proving for generalized Frobenius algebras. Such computations and theorem proving can be performed automatically using the Automated Theorem Provers with the TPTP language and the SMT-solver Z3 with the SMT-LIB language. Some examples of application of ATPs and SMT-solvers in the mathematical setup of an open-closed stringy topological quantum computer will be provided.
Classical Gelfand duality provides an equivalence between commutative C-star algebras and topological spaces, but fails to furnish a geometric object for noncommutative operator systems. To address this, we introduce a categorified notion of spectrum that captures the full operator-semantic structure. For an operator system A, we construct a spectral stack, denoted Spec(A), over the site of its commutative contexts. The construction proceeds in three stages. First, we encode the syntax of A via a colored operad called the synergy operad. Second, we aggregate local semantic data using a left Kan extension, providing an explicit coend formula. Third, we enforce descent via sheafification, yielding a stack that satisfies higher gluing conditions. We prove that Spec(A) satisfies a Yoneda-style universal property, making it the initial descent-complete semantic realization of A. This yields a contravariant functor from operator systems to spectral objects that admits a right adjoint, the global sections functor. Under semantic generation and descent completeness, the counit of this adjunction is an equivalence, establishing a reconstruction theorem: A is isomorphic to the endomorphisms of the structure sheaf on its spectrum. We further provide a recognition theorem characterizing the essential image of this functor and prove Morita invariance of the associated quasi-coherent sheaf categories. The construction naturally recovers classical Gelfand spectra and Bohrification as truncations of a Postnikov tower. Explicit computations for matrix algebras, Pauli systems, and the Mermin-Peres square yield a quantitative invariant of contextuality extracted from the inertia stack of Spec(A). Comparison theorems show that our framework subsumes Gelfand duality, Bohrification, and Tannaka reconstruction as special cases.
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M in [28] constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.