Pith. sign in

REVIEW 5 major objections 5 minor 57 references

Quantum control of higher-order functions can be typed so that every definable first-order program is an isometry.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 21:54 UTC pith:VGWDFF4H

load-bearing objection A genuinely new causality paradox and a clever BV-based type system, but the central soundness proof leans on an unproven monadicity lemma and the full-abstraction claim overreaches. the 5 major comments →

arxiv 2607.15926 v1 pith:VGWDFF4H submitted 2026-07-17 cs.PL cs.LOquant-ph

Causality in Pure Quantum Computation with Quantum Control

Kengo Hirata , Takeshi Tsukada This is my paper
classification cs.PL cs.LOquant-ph MSC 03B4703F5268Q12
keywords quantum controlsupermapBV logiccausal structurelambda calculuscategorical semanticspure quantum computationlinear logic
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces λqif, a higher-order quantum programming language with quantum conditional branching (qif), and argues that its type system excludes programs that would violate physical causality. The central move is to type qif terms as qbit▷A, meaning the control qubit becomes available only after the branch result A is resolved, instead of the naïve qbit⊗A. This blocks programs such as one that applies a controlled-NOT to its own control qubit, whose denotation would be a non-unitary, physically unrealizable linear map. The authors construct a categorical model, CausHilb, that interprets the causal types, and show that every term of first-order type denotes an isometry and that the OCB process — a well-known non-pure supermap — is not definable.

Core claim

The paper's central claim is that combining higher-order functions with quantum control creates a new causality hazard: a term can route its own control qubit back into the controlled function, forming a closed timelike curve and denoting a non-unitary map in the standard Hilb semantics. By reading the type of qif as qbit▷A and by marking first-order types (qudits) that validate the isomorphisms F⊗A ≅ F◁A and F⊸(C◁A) ≅ (F⊸C)◁A, the language becomes causally safe. Concretely, every term of type qbit⊸qbit denotes a unitary transformation (Proposition 39), and the definable supermaps are exactly the pure supermaps, so the OCB process is excluded (Theorem 40).

What carries the argument

The load-bearing machinery is the seq-connective ◁ from BV/pomset logic, read as 'happens before', together with a first-order-type discipline. In λqif, the quantum conditional is typed qif M then N₁ else N₂ : qbit▷A, deferring the control qubit until the branch result A is resolved; first-order types (qudits and units) validate the isomorphisms that let programs like the controlled-NOT be expressed. The semantic carrier is the category CausHilb, defined as a pullback of a causal-semantics construction on completely positive maps along the embedding from Hilb; this category is shown to be a BV-category, and its first-order objects are exactly the isometries.

Load-bearing premise

The proof that CausHilb is a BV-category relies on Lemma 28 — that BV-categories are finitary monadic over Cat — whose proof is only a sketch; if that monadicity or the pullback preservation it implies fails, the causal semantics may not validate the typing rules.

What would settle it

Type the program from the introduction that applies a qif-generated function to its own control qubit and compute its denotation; the paper predicts it is rejected by the type system, so any well-typed derivation — or any typed qbit⊸qbit term whose Hilb denotation is the non-unitary matrix [[1,0],[1,0]] — would falsify Proposition 39.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Every λqif program of type qbit⊸qbit denotes a unitary transformation, so the language cannot express non-unitary qubit-level effects.
  • The OCB process is not definable in λqif; the only indefinite causal order expressible is the pure kind exemplified by the quantum SWITCH.
  • All pure supermaps with one or two inputs are definable (using a generalized qudit-qif), so the type system captures the known pure-supermap classes up to two inputs.
  • Full abstraction holds without an operational semantics: two terms are indistinguishable in all qubit-typed contexts exactly when they have the same denotation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The 'defer the control resource until the branch is resolved' discipline is a general pattern; it should transfer to other higher-order settings where a reusable resource (a classical bit, an effect token) must be recombined after branching.
  • The pullback recipe behind CausHilb — glueing a pure category to a causal category along an embedding — may yield causal models for other pure quantum subtheories, such as stabilizer or Clifford computation.
  • If the conjecture about tripartite supermaps is correct, the boundary between qif-definable and causally admissible processes first appears at three inputs, giving a natural expressiveness measure for quantum control.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

5 major / 5 minor

Summary. The paper proposes a typed lambda calculus, λqif, for pure quantum computation with higher-order functions and quantum conditional branching. The type system is based on intuitionistic BV logic extended with first-order types, and the qif rule is typed as qbit▷A rather than qbit⊗A in order to prevent causally paradoxical programs such as the closed-timelike-curve example (∗∗). The authors give a degenerate denotational semantics in Hilb and then construct a more refined categorical model CausHilb as a pullback of Caus[CPM] and Hilb. They claim that this model interprets BV logic and the type system, that every first-order term of type n⊸m denotes an isometry (Prop. 39), that definable supermaps are pure and hence the OCB process is not definable (Thm. 40), and that the semantics is fully abstract with respect to qudit-typed contexts (Thm. 38).

Significance. If the proof gaps are closed, this would be a valuable contribution: it gives a concrete syntax-directed account of causality in higher-order quantum computation, connects quantum control with BV/causal logic, and provides a new categorical model that separates pure from non-pure supermaps. The central idea of typing qif with qbit▷A and using first-order types is elegant, and the paper includes useful examples (SWITCH, causally ordered composition, two-slot supermaps). The full-abstraction statement and the definability characterizations are ambitious and, if fully justified, would substantially strengthen the programming-language semantics literature for quantum computation.

major comments (5)
  1. [§5.3, Lemma 28 and Corollary 29] The monadicity of the category of BV-categories over Cat is load-bearing: Corollary 29 uses it to transfer BV-structure along the pullback defining CausHilb. The proof is only a sketch asserting that the theory is a TCat-relative algebraic theory; the needed partial Horn theory and the verification that all coherence diagrams (including the duoidal interchange ζ and its coherence laws) are equations of that theory are not supplied. Since Prop. 33 and therefore the interpretation of ◁, await, and expose depend on this, please give a complete proof or verify the BV coherence axioms directly for CausHilb.
  2. [§5.4, Proposition 33] The proof that the maps ξ_{A,B} and γ_{B,C,A} are isomorphisms for first-order A relies on the assertion that the embedding CausHilb→Caus[CPM] is conservative and on the claim that the inverse is obtained from a derivation in causal logic. Conservativity is stated without proof. Because the term semantics uses ξ^{-1} and γ^{-1} for await and expose, this is a central point. Please prove conservativity explicitly, or construct the inverses directly as claimed in Remark 34.
  3. [§6.1 and Appendix C, Proposition 35] The proof of the qif lift appears to check the wrong causal condition. The type of qif is qbit▷A = A◁qbit, so the causal set c_{A◁qbit} requires, for all π∈c_2^*, the morphism (id_A⊗π) applied to the output to lie in c_A. The appendix instead applies π⊗id_A and concludes membership in c_2 (with an apparent typo 'ρ2∈c_A'). Moreover the output of qif_A is ordered 2⊗A while the object A◁2 has underlying A⊗2; the symmetry identification is not stated. As written, Proposition 35 is not established. Please correct the order and the quantifier/target of the causal condition, or give a direct verification.
  4. [§6.2, Lemma 36] Lemma 36 states that for every d there is a closed term H_d:d⊗d whose semantics is (1/√d)η_d, but no proof or construction is given. Lemma 37 and Theorem 38 (full abstraction) rely on this lemma. Even if the construction is straightforward using qif and state preparation, it should be written out, since the existence of such a term is not obvious from the primitive set (which includes injections and unitaries but no explicit entanglement constructor).
  5. [§6.3, Propositions 41-42 and Theorem 40] The definability theorems for one- and two-input supermaps are delegated to external results [15, Theorem 1] and [56, Theorem 5], and Theorem 40 also depends on [56] for the necessity direction. Please state precisely which theorems are being invoked, verify that their hypotheses (e.g., domain dimensions, auxiliary systems, determinism, pure versus CP maps) match the present definition of pure supermaps, and explain how the cited normal forms are represented by the primitives of λqif, including the generalized qif. Without this, the claim that the OCB process is not definable is only as strong as the unstated correspondence between CausHilb morphisms and pure supermaps.
minor comments (5)
  1. [Appendix C, proof of Prop. 35] There is a quantifier typo: '∀ρ2∈c_A' should read '∀ρ2∈c_2', and the final membership '∈c_2' in the displayed display should presumably be '∈c_A' (modulo the order issue raised above).
  2. [Figure 7] The semantics of qif is written as qif_A∘(JMK⊗⟨JN1K,JN2K⟩), but the typing rule gives the result type qbit▷A = A◁qbit. Please state explicitly which symmetry isomorphism identifies the codomain 2⊗A with A⊗2.
  3. [Remark 8] The paper deliberately omits an operational semantics. This is acceptable for a denotational study, but readers should be told more clearly that 'programming language' here means a typed term calculus with a categorical semantics, not a language with reduction rules.
  4. [Remark 25] The claim that CausHilb together with the forgetful functor to Hilb is a strong BV-category is asserted without proof. If this is needed for the soundness claim for BV-logic, a proof or a precise reference to the coherence axioms should be provided; otherwise it should be marked as a conjecture.
  5. [§4.3, Example 12] The example claims that a certain term 'cannot be represented in a language that separates control and target qubits as in [17]'. This comparison would be more useful if the precise class of languages in [17] were briefly described.

Circularity Check

0 steps flagged

No circularity: the causal guarantee is obtained from an independently constructed categorical model, not from the typing rules by construction.

full rationale

I traced the main derivation chain: the language is interpreted in CausHilb, a pullback of Hilb and Caus[CPM] (Definition 20, Lemma 21), using the independently developed Caus construction and external monadicity facts. The central isometry theorem (Prop. 39) follows from Theorem 31, which computes the hom-category of first-order objects as Isom; this is a semantic fact, not a property imposed into the typing rules. The qif rule is typed at qbit▷A (Fig. 4), and the soundness of qif in CausHilb is proved separately (Prop. 35). The first-order isomorphisms needed for await/expose (Prop. 33) are transferred from Caus[CPM] via conservativity, and the BV-category structure is obtained from an external monadicity theorem (Lemma 28, Cor. 29). Some supporting lemmas are only sketched or are cited from external work (Lemma 28; conservativity in Section 5.4; Remark 25 notes that BV-category soundness is partially open and cites [4]), but these are proof-quality and dependency gaps, not circularity. Theorem 40's exclusion of OCB rests on the external fact that OCB is not pure [6] together with an independent purity characterization; it is not a restatement of a typing rule. No equation in the paper reduces a predicted quantity to a fitted input, and there are no load-bearing self-citations. I therefore find no circular step under the stated criteria.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

The central claim rests on external theories (Caus construction, monadicity of BV-categories, pure supermap classification) and on the standard physical classification of realizable supermaps. No numerical free parameters appear; the new formal constructs (λqif, CausHilb) are the paper's contribution and are not ad hoc physical entities.

axioms (6)
  • domain assumption Caus construction (Kissinger-Uijlen, Simmons-Kissinger) produces a BV-category with first-order objects from an additive precausal category, and Caus[CPM] models quantum causal structure.
    Fundamental to defining CausHilb as a pullback and inheriting the ◁-structure and first-order objects (Sections 5.1-5.4, Theorem 27 [50]).
  • domain assumption The category of BV-categories is finitary monadic over Cat (Lemma 28), so the pullback in diagram (2) preserves BV-structure.
    Proof is only a sketch relying on [33] and [42]; Corollary 29 depends on it to conclude CausHilb is a BV-category.
  • domain assumption Pure supermaps are exactly those of the form ιf with f∈CausHilb; deterministic supermaps have the form λf.V(f⊗id)U·inj [15, Thm 1]; bipartite pure supermaps decompose as direct sums of causally ordered combs [56, Thm 5].
    Used in Theorem 40 and Propositions 41-42; proofs are not given in this paper, only references.
  • domain assumption A physically realizable linear map of type qbit⊸qbit is unitary, and the OCB process is not pure and hence suspected unrealizable [6,40].
    Motivates the target: type system should rule out non-unitary definable maps (Section 1) and OCB (Section 6.3).
  • standard math The category AutCat of ∗-autonomous categories is monadic over Cat, so the forgetful functor creates limits (Blackwell-Kelly-Power [11]).
    Used in Proposition 22 to prove CausHilb is ∗-autonomous.
  • standard math IBV and the simplified sequent calculus sequentIBV are equi-expressive (Prop 5), and each sequentIBV proof yields a λqif term (Prop 7).
    Basis for the Curry-Howard reading of the type system; proofs sketched in Appendix A.

pith-pipeline@v1.3.0-alltime-deepseek · 30332 in / 19784 out tokens · 199413 ms · 2026-08-01T21:54:37.418318+00:00 · methodology

0 comments
read the original abstract

Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

57 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    Abbott, Christina Giarmatzi, Fabio Costa, and Cyril Branciard

    Alastair A. Abbott, Christina Giarmatzi, Fabio Costa, and Cyril Branciard. Multipartite causal correlations: Polytopes and inequalities. Phys. Rev. A , 94:032131, Sep 2016. URL: https://link.aps.org/doi/10.1103/PhysRevA.94.032131, https://doi.org/10.1103/PhysRevA.94.032131 doi:10.1103/PhysRevA.94.032131

    work page doi:10.1103/physreva.94.032131 2016

  2. [2]

    Proofs as execution trees for the -calculus, 2025

    Matteo Acclavio and Giulia Manara. Proofs as execution trees for the -calculus, 2025. URL: https://arxiv.org/abs/2411.08847, https://arxiv.org/abs/2411.08847 arXiv:2411.08847

    Pith/arXiv arXiv 2025

  3. [3]

    Intuitionistic BV

    Matteo Acclavio and Lutz Stra burger. Intuitionistic BV . In Gian Luca Pozzato and Tarmo Uustalu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27-29, 2025, Proceedings , volume 15980 of Lecture Notes in Computer Science , pages 414--432. Springer, 2025...

    work page doi:10.1007/978-3-032-06085-3_22 2025

  4. [4]

    Proof identity and categorical models of BV

    Matteo Acclavio, Lutz Stra burger, and Vladimir Zamdzhiev. Proof identity and categorical models of BV . In Frank Pfenning, editor, 11th International Conference on Formal Structures for Computation and Deduction ( FSCD 2026) , volume 378 of Leibniz International Proceedings in Informatics ( LIPIcs ) . Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informati...

    Pith/arXiv arXiv 2026

  5. [5]

    Computational advantage from quantum-controlled ordering of gates

    Mateus Ara \' u jo, Fabio Costa, and C aslav Brukner. Computational advantage from quantum-controlled ordering of gates. Physical Review Letters , 113(25):250402, dec 2014. https://doi.org/10.1103/physrevlett.113.250402 doi:10.1103/physrevlett.113.250402

    doi:10.1103/physrevlett.113.250402 2014

  6. [6]

    A purification postulate for quantum mechanics with indefinite causal order

    Mateus Ara \' u jo, Adrien Feix, Miguel Navascu \' e s, and Caslav Brukner. A purification postulate for quantum mechanics with indefinite causal order. Quantum , 1:10, 2017. URL: https://doi.org/10.22331/q-2017-04-26-10, https://doi.org/10.22331/Q-2017-04-26-10 doi:10.22331/Q-2017-04-26-10

    work page doi:10.22331/q-2017-04-26-10 2017

  7. [7]

    Witnessing causal nonseparability

    Mateus Araújo, Cyril Branciard, Fabio Costa, Adrien Feix, Christina Giarmatzi, and Časlav Brukner. Witnessing causal nonseparability. New Journal of Physics , 17(10):102001, oct 2015. https://doi.org/10.1088/1367-2630/17/10/102001 doi:10.1088/1367-2630/17/10/102001

    work page doi:10.1088/1367-2630/17/10/102001 2015

  8. [8]

    *-autonomous categories and linear logic

    Michael Barr. *-autonomous categories and linear logic. Math. Struct. Comput. Sci. , 1(2):159--178, 1991. https://doi.org/10.1017/S0960129500001274 doi:10.1017/S0960129500001274

    work page doi:10.1017/s0960129500001274 1991

  9. [9]

    Maximal incompatibility of locally classical behavior and global causal order in multiparty scenarios

    \"Amin Baumeler, Adrien Feix, and Stefan Wolf. Maximal incompatibility of locally classical behavior and global causal order in multiparty scenarios. Phys. Rev. A , 90:042106, Oct 2014. URL: https://link.aps.org/doi/10.1103/PhysRevA.90.042106, https://doi.org/10.1103/PhysRevA.90.042106 doi:10.1103/PhysRevA.90.042106

    doi:10.1103/physreva.90.042106 2014

  10. [10]

    The space of logically consistent classical processes without causal order

    Ämin Baumeler and Stefan Wolf. The space of logically consistent classical processes without causal order. New Journal of Physics , 18(1):013036, jan 2016. https://doi.org/10.1088/1367-2630/18/1/013036 doi:10.1088/1367-2630/18/1/013036

    doi:10.1088/1367-2630/18/1/013036 2016

  11. [11]

    Two-dimensional monad theory

    Robert Blackwell, Gregory M Kelly, and A John Power. Two-dimensional monad theory. Journal of Pure and Applied Algebra , 59(1):1--41, 1989. URL: https://www.sciencedirect.com/science/article/pii/0022404989901606, https://doi.org/10.1016/0022-4049(89)90160-6 doi:10.1016/0022-4049(89)90160-6

    arXiv 1989

  12. [12]

    Deep inference and probabilistic coherence spaces

    Richard Blute, Prakash Panangaden, and Sergey Slavnov. Deep inference and probabilistic coherence spaces. Applied Categorical Structures , 20(3):209--228, 2012. https://doi.org/10.1007/s10485-010-9241-0 doi:10.1007/s10485-010-9241-0

    work page doi:10.1007/s10485-010-9241-0 2012

  13. [13]

    The simplest causal inequalities and their violation

    Cyril Branciard, Mateus Araújo, Adrien Feix, Fabio Costa, and Časlav Brukner. The simplest causal inequalities and their violation. New Journal of Physics , 18(1):013008, dec 2015. https://doi.org/10.1088/1367-2630/18/1/013008 doi:10.1088/1367-2630/18/1/013008

    work page doi:10.1088/1367-2630/18/1/013008 2015

  14. [14]

    Indefinite causal order enables perfect quantum communication with zero capacity channels

    Giulio Chiribella, Manik Banik, Some Sankar Bhattacharya, Tamal Guha, Mir Alimuddin, Arup Roy, Sutapa Saha, Sristy Agrawal, and Guruprasad Kar. Indefinite causal order enables perfect quantum communication with zero capacity channels. New Journal of Physics , 23(3):033039, March 2021. https://doi.org/10.1088/1367-2630/abe7a0 doi:10.1088/1367-2630/abe7a0

    doi:10.1088/1367-2630/abe7a0 2021

  15. [15]

    Transforming quantum operations: Quantum supermaps

    Giulio Chiribella, Giacomo Mauro D'Ariano, and Paolo Perinotti. Transforming quantum operations: Quantum supermaps. Europhysics Letters , 83(3):30004, jul 2008. https://doi.org/10.1209/0295-5075/83/30004 doi:10.1209/0295-5075/83/30004

    doi:10.1209/0295-5075/83/30004 2008

  16. [16]

    Quantum computations without definite causal structure

    Giulio Chiribella, Giacomo Mauro D'Ariano, Paolo Perinotti, and Benoit Valiron. Quantum computations without definite causal structure. Physical Review A , 88(2):022318, aug 2013. https://doi.org/10.1103/physreva.88.022318 doi:10.1103/physreva.88.022318

    doi:10.1103/physreva.88.022318 2013

  17. [17]

    PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations

    Alexandre Cl \'e ment and Simon Perdrix. PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations . In Javier Esparza and Daniel Kr \'a ľ, editors, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) , volume 170 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 24:1--24:14, Da...

    2020

  18. [18]

    Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories

    J Robin B Cockett and Robert AG Seely. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory and Applications of categories , 3(5):85--131, 1997

    1997

  19. [19]

    Quantum computation with programmable connections between gates

    Timoteo Colnaghi, Giacomo Mauro D'Ariano, Stefano Facchini, and Paolo Perinotti. Quantum computation with programmable connections between gates. Physics Letters A , 376(45):2940--2943, October 2012. https://doi.org/10.1016/j.physleta.2012.08.028 doi:10.1016/j.physleta.2012.08.028

    work page doi:10.1016/j.physleta.2012.08.028 2012

  20. [20]

    Enhanced communication with the assistance of indefinite causal order

    Daniel Ebler, Sina Salek, and Giulio Chiribella. Enhanced communication with the assistance of indefinite causal order. Physical Review Letters , 120(12):120502, March 2018. https://doi.org/10.1103/physrevlett.120.120502 doi:10.1103/physrevlett.120.120502

    doi:10.1103/physrevlett.120.120502 2018

  21. [21]

    Causally nonseparable processes admitting a causal model

    Adrien Feix, Mateus Araújo, and Časlav Brukner. Causally nonseparable processes admitting a causal model. New Journal of Physics , 18(8):083040, aug 2016. https://doi.org/10.1088/1367-2630/18/8/083040 doi:10.1088/1367-2630/18/8/083040

    work page doi:10.1088/1367-2630/18/8/083040 2016

  22. [22]

    Nicolai Friis, Vedran Dunjko, Wolfgang D \"u r, and Hans J. Briegel. Implementing quantum control for unknown subroutines. Physical Review A , 89(3):030303, mar 2014. https://doi.org/10.1103/physreva.89.030303 doi:10.1103/physreva.89.030303

    doi:10.1103/physreva.89.030303 2014

  23. [23]

    Linear logic

    Jean-Yves Girard. Linear logic. Theoretical Computer Science , 50(1):1--101, 1987. URL: https://www.sciencedirect.com/science/article/pii/0304397587900454, https://doi.org/10.1016/0304-3975(87)90045-4 doi:10.1016/0304-3975(87)90045-4

    arXiv 1987

  24. [24]

    A system of interaction and structure

    Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic , 8(1):1, January 2007. https://doi.org/10.1145/1182613.1182614 doi:10.1145/1182613.1182614

    arXiv 2007

  25. [25]

    A system of interaction and structure v: The exponentials and splitting

    Alessio Guglielmi and Lutz Stra burger. A system of interaction and structure v: The exponentials and splitting. Mathematical. Structures in Comp. Sci. , 21(3):563--584, June 2011. https://doi.org/10.1017/S096012951100003X doi:10.1017/S096012951100003X

    work page doi:10.1017/s096012951100003x 2011

  26. [26]

    A Profunctorial Semantics for Quantum Supermaps

    James Hefford and Matt Wilson. A profunctorial semantics for quantum supermaps, 2024. https://doi.org/10.48550/ARXIV.2402.02997 doi:10.48550/ARXIV.2402.02997

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2402.02997 2024

  27. [27]

    A bv-category of spacetime interventions

    James Hefford and Matthew Wilson. A bv-category of spacetime interventions. CoRR , abs/2502.19022, 2025. URL: https://doi.org/10.48550/arXiv.2502.19022, https://arxiv.org/abs/2502.19022 arXiv:2502.19022 , https://doi.org/10.48550/ARXIV.2502.19022 doi:10.48550/ARXIV.2502.19022

    Pith/arXiv arXiv doi:10.48550/arxiv.2502.19022 2025

  28. [28]

    Concurrent kleene algebra and its foundations

    Tony Hoare, Bernhard M \" o ller, Georg Struth, and Ian Wehrman. Concurrent kleene algebra and its foundations. J. Log. Algebraic Methods Program. , 80(6):266--296, 2011. URL: https://doi.org/10.1016/j.jlap.2011.04.005, https://doi.org/10.1016/J.JLAP.2011.04.005 doi:10.1016/J.JLAP.2011.04.005

    work page doi:10.1016/j.jlap.2011.04.005 2011

  29. [29]

    Projective characterization of higher-order quantum transformations, 2024

    Timothée Hoffreumon and Ognyan Oreshkov. Projective characterization of higher-order quantum transformations, 2024. URL: http://arxiv.org/abs/2206.06206, https://arxiv.org/abs/2206.06206 [quant-ph] arXiv:2206.06206 [quant-ph] , https://doi.org/10.48550/arXiv.2206.06206 doi:10.48550/arXiv.2206.06206

    doi:10.48550/arxiv.2206.06206 2024

  30. [30]

    Constructing weak simulations from linear implications for processes with private names

    Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Math. Struct. Comput. Sci. , 29(8):1275--1308, 2019. https://doi.org/10.1017/S0960129518000452 doi:10.1017/S0960129518000452

    work page doi:10.1017/s0960129518000452 2019

  31. [31]

    Glueing and orthogonality for models of linear logic

    Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science , 294(1):183--231, 2003. Category Theory and Computer Science. URL: https://www.sciencedirect.com/science/article/pii/S0304397501002419, https://doi.org/10.1016/S0304-3975(01)00241-9 doi:10.1016/S0304-3975(01)00241-9

    doi:10.1016/s0304-3975(01)00241-9 2003

  32. [32]

    On the structure of higher order quantum maps, 2026

    Anna Jenčová. On the structure of higher order quantum maps, 2026. URL: https://arxiv.org/abs/2411.09256, https://arxiv.org/abs/2411.09256 arXiv:2411.09256

    Pith/arXiv arXiv 2026

  33. [33]

    Relativized universal algebra via partial horn logic

    Yuto Kawase. Relativized universal algebra via partial horn logic. Theory and Applications of Categories , 45(18):660--716, March 2026. Published 2026-03-27. URL: http://www.tac.mta.ca/tac/volumes/45/18/45-18.pdf

    2026

  34. [34]

    A categorical semantics for causal structure

    Aleks Kissinger and Sander Uijlen. A categorical semantics for causal structure. LMCS , 15(3), 2019. https://doi.org/10.48550/ARXIV.1701.04732 doi:10.48550/ARXIV.1701.04732

    Pith/arXiv arXiv doi:10.48550/arxiv.1701.04732 2019

  35. [35]

    Resource theories of communication

    Hl \' e r Kristj \' a nsson, Giulio Chiribella, Sina Salek, Daniel Ebler, and Matthew Wilson. Resource theories of communication. New Journal of Physics , 22(7):073014, jul 2020. https://doi.org/10.1088/1367-2630/ab8ef7 doi:10.1088/1367-2630/ab8ef7

    work page doi:10.1088/1367-2630/ab8ef7 2020

  36. [36]

    Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits, 2024

    Hl \'e r Kristj \'a nsson, Tatsuki Odake, Satoshi Yoshida, Philip Taranto, Jessica Bavaresco, Marco T \'u lio Quintino, and Mio Murao. Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits, 2024. https://doi.org/10.48550/ARXIV.2409.18420 doi:10.48550/ARXIV.2409.18420

    Pith/arXiv arXiv doi:10.48550/arxiv.2409.18420 2024

  37. [37]

    Quantum coherence spaces revisited: A von neumann (co)algebraic approach

    Thea Li and Vladimir Zamdzhiev. Quantum coherence spaces revisited: A von neumann (co)algebraic approach. In Nathalie Bertrand and Stefan Milius, editors, Foundations of Software Science and Computation Structures , pages 418--439, Cham, 2026. Springer Nature Switzerland

    2026

  38. [38]

    Experimentally demonstrating indefinite causal order algorithms to solve the generalized deutsch’s problem

    Wen‐Qiang Liu, Zhe Meng, Bo‐Wen Song, Jian Li, Qing‐Yuan Wu, Xiao‐Xiao Chen, Jin‐Yang Hong, An‐Ning Zhang, and Zhang‐Qi Yin. Experimentally demonstrating indefinite causal order algorithms to solve the generalized deutsch’s problem. Advanced Quantum Technologies , August 2024. https://doi.org/10.1002/qute.202400181 doi:10.1002/qute.202400181

    work page doi:10.1002/qute.202400181 2024

  39. [39]

    A system of interaction and structure III: the complexity of BV and pomset logic

    L \^ e Th \` a nh Dung Nguy \^ e n and Lutz Stra burger. A system of interaction and structure III: the complexity of BV and pomset logic. Log. Methods Comput. Sci. , 19(4), 2023. URL: https://doi.org/10.46298/lmcs-19(4:25)2023, https://doi.org/10.46298/LMCS-19(4:25)2023 doi:10.46298/LMCS-19(4:25)2023

    work page doi:10.46298/lmcs-19(4:25)2023 2023

  40. [40]

    Quantum correlations with no causal order

    Ognyan Oreshkov, Fabio Costa, and Časlav Brukner. Quantum correlations with no causal order. Nature Communications , 3(1), October 2012. https://doi.org/10.1038/ncomms2076 doi:10.1038/ncomms2076

    doi:10.1038/ncomms2076 2012

  41. [41]

    Causal and causally separable processes

    Ognyan Oreshkov and Christina Giarmatzi. Causal and causally separable processes. New Journal of Physics , 18(9):093020, sep 2016. https://doi.org/10.1088/1367-2630/18/9/093020 doi:10.1088/1367-2630/18/9/093020

    doi:10.1088/1367-2630/18/9/093020 2016

  42. [42]

    Erik Palmgren and Steven J. Vickers. Partial horn logic and cartesian categories. Ann. Pure Appl. Log. , 145(3):314--353, 2007. URL: https://doi.org/10.1016/j.apal.2006.10.001, https://doi.org/10.1016/J.APAL.2006.10.001 doi:10.1016/J.APAL.2006.10.001

    doi:10.1016/j.apal.2006.10.001 2007

  43. [43]

    Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads

    Hugo Paquet and Philip Saville. Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024 , pages 61:1--61:15. ACM , 2024. https://doi.org/...

    arXiv 2024

  44. [44]

    Procopio, Amir Moqanaki, Mateus Ara \' u jo, Fabio Costa, Irati Alonso Calafell, Emma G

    Lorenzo M. Procopio, Amir Moqanaki, Mateus Ara \' u jo, Fabio Costa, Irati Alonso Calafell, Emma G. Dowd, Deny R. Hamel, Lee A. Rozema, C aslav Brukner, and Philip Walther. Experimental superposition of orders of quantum gates. Nature Communications , 6(1), aug 2015. https://doi.org/10.1038/ncomms8913 doi:10.1038/ncomms8913

    doi:10.1038/ncomms8913 2015

  45. [45]

    Tom Purves and Anthony J. Short. Quantum theory cannot violate a causal inequality. Phys. Rev. Lett. , 127:110402, Sep 2021. URL: https://link.aps.org/doi/10.1103/PhysRevLett.127.110402, https://doi.org/10.1103/PhysRevLett.127.110402 doi:10.1103/PhysRevLett.127.110402

    work page doi:10.1103/physrevlett.127.110402 2021

  46. [46]

    Pomset logic: A non-commutative extension of classical linear logic

    Christian Retor \' e . Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote, editor, Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings , volume 1210 of Lecture Notes in Computer Science , pages 300--318....

    work page doi:10.1007/3-540-62688-3_43 1997

  47. [47]

    Pomset logic: a logical and grammatical alternative to the lambek calculus

    Christian Retor \' e . Pomset logic: a logical and grammatical alternative to the lambek calculus. CoRR , abs/2001.02155, 2020. URL: http://arxiv.org/abs/2001.02155, https://arxiv.org/abs/2001.02155 arXiv:2001.02155

    Pith/arXiv arXiv 2001

  48. [48]

    Towards a quantum programming language

    Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science , 14(4):527--586, aug 2004. https://doi.org/10.1017/s0960129504004256 doi:10.1017/s0960129504004256

    doi:10.1017/s0960129504004256 2004

  49. [49]

    Towards a semantics for higher-order quantum computation

    Peter Selinger. Towards a semantics for higher-order quantum computation. In Proceedings of the 2nd International Workshop on Quantum Programming Languages , pages 127--143, 2004

    2004

  50. [50]

    Higher-order causal theories are models of bv-logic, 2022

    Will Simmons and Aleks Kissinger. Higher-order causal theories are models of bv-logic, 2022. https://doi.org/10.48550/ARXIV.2205.11219 doi:10.48550/ARXIV.2205.11219

    Pith/arXiv arXiv doi:10.48550/arxiv.2205.11219 2022

  51. [51]

    A complete logic for causal consistency

    Will Simmons and Aleks Kissinger. A complete logic for causal consistency. CoRR , abs/2403.09297, 2024. URL: https://doi.org/10.48550/arXiv.2403.09297, https://arxiv.org/abs/2403.09297 arXiv:2403.09297 , https://doi.org/10.48550/ARXIV.2403.09297 doi:10.48550/ARXIV.2403.09297

    Pith/arXiv arXiv doi:10.48550/arxiv.2403.09297 2024

  52. [52]

    A system of interaction and structure iv: The exponentials and decomposition

    Lutz Stra burger and Alessio Guglielmi. A system of interaction and structure iv: The exponentials and decomposition. ACM Trans. Comput. Logic , 12(4), July 2011. https://doi.org/10.1145/1970398.1970399 doi:10.1145/1970398.1970399

    arXiv 2011

  53. [53]

    Taddei, Jaime Cari \ n e, Daniel Mart \' nez, Tania Garc \' a, Nayda Guerrero, Alastair A

    M \' a rcio M. Taddei, Jaime Cari \ n e, Daniel Mart \' nez, Tania Garc \' a, Nayda Guerrero, Alastair A. Abbott, Mateus Ara \' u jo, Cyril Branciard, Esteban S. G \' o mez, Stephen P. Walborn, Leandro Aolita, and Gustavo Lima. Computational advantage from the quantum superposition of multiple temporal orders of photonic gates. PRX Quantum , 2(1):010320, ...

    doi:10.1103/prxquantum.2.010320 2021

  54. [54]

    A system of interaction and structure II: the need for deep inference

    Alwen Tiu. A system of interaction and structure II: the need for deep inference. Log. Methods Comput. Sci. , 2(2), 2006. https://doi.org/10.2168/LMCS-2(2:4)2006 doi:10.2168/LMCS-2(2:4)2006

    doi:10.2168/lmcs-2(2:4)2006 2006

  55. [55]

    Abbott, and Cyril Branciard

    Julian Wechs, Hippolyte Dourdent, Alastair A. Abbott, and Cyril Branciard. Quantum circuits with classical versus quantum control of causal order. PRX Quantum , 2(3):030335, August 2021. https://doi.org/10.1103/prxquantum.2.030335 doi:10.1103/prxquantum.2.030335

    doi:10.1103/prxquantum.2.030335 2021

  56. [56]

    Consequences of preserving reversibility in quantum superchannels

    Wataru Yokojima, Marco T \' u lio Quintino, Akihito Soeda, and Mio Murao. Consequences of preserving reversibility in quantum superchannels. Quantum , 5:441, April 2021. https://doi.org/10.22331/q-2021-04-26-441 doi:10.22331/q-2021-04-26-441

    doi:10.22331/q-2021-04-26-441 2021

  57. [57]

    Charging quantum batteries via indefinite causal order: Theory and experiment

    Gaoyan Zhu, Yuanbo Chen, Yoshihiko Hasegawa, and Peng Xue. Charging quantum batteries via indefinite causal order: Theory and experiment. Phys. Rev. Lett. , 131:240401, Dec 2023. URL: https://link.aps.org/doi/10.1103/PhysRevLett.131.240401, https://doi.org/10.1103/PhysRevLett.131.240401 doi:10.1103/PhysRevLett.131.240401

    work page doi:10.1103/physrevlett.131.240401 2023