Pith. sign in

REVIEW 2 major objections 4 minor 52 references

A linear quantum language makes indefinite causal order, including the quantum switch with measurements, well-typed and physically sound.

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 · grok-4.5

2026-07-13 02:18 UTC pith:GS5ZUMQR

load-bearing objection Solid, carefully engineered language that finally puts linear ICO + measurement on a sound operational and causal footing; the extra qcase discipline is the real technical price of admission. the 2 major comments →

arxiv 2607.09534 v1 pith:GS5ZUMQR submitted 2026-07-10 cs.LO quant-ph

Higher-Order Programs with Indefinite Causal Orders: a Linear Approach to Coherent Control of Quantum Processes

Kathleen Barsse , Romain P\'echoux , Simon Perdrix This is my paper
classification cs.LO quant-ph MSC 68N1818M4581P68
keywords indefinite causal orderquantum switchlinear quantum programminghigher-order quantum mapsCaus[CPM]QC-QCcoherent controldevice references
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.

Processes that put the order of quantum operations into superposition (indefinite causal orders) give real computational advantages, yet existing quantum languages either ban measurement or implement control nonlinearly and therefore lose those advantages. This paper defines a higher-order functional language whose linear type system treats coherent control correctly on arbitrary quantum channels, not just unitaries. Device references and a memory function keep measurement outcomes synchronized across superposed branches; a denotational semantics in the causal category Caus[CPM] guarantees that every well-typed program denotes a physically meaningful higher-order process. The language realises every first-order quantum channel and a large second-order class of quantum circuits with quantum control that contains the quantum switch; the same design extends cleanly to recursion and controlled non-linearity.

Core claim

A higher-order linear quantum language with a carefully restricted qcase construct, operationalised by device references and memory functions, is sound with respect to Caus[CPM]; every well-typed term is therefore a physically valid higher-order quantum process, and the language realises every quantum channel at first order together with every QC-QC-with-memory (including the quantum switch) at second order.

What carries the argument

The linear qcase typing rule (branches must be controllable terms of type A ⊸ q^n) together with the operational device-reference/memory mechanism that forces identical measurement outcomes across superposed copies of the same channel; their joint denotation lands inside Caus[CPM].

Load-bearing premise

Branches of quantum control may not themselves contain free measurements and must return only qubits, otherwise the denotation can leave the set of physical higher-order maps.

What would settle it

Exhibit a well-typed term whose denotation fails to be a morphism of Caus[CPM], or a QC-QC-with-memory that cannot be expressed by any well-typed term of the language.

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

If this is right

  • Physicality of any program is decidable by ordinary type-checking in polynomial time; no separate unitarity or orthogonality test is required.
  • The quantum switch and its generalisations can be written as ordinary higher-order programs and composed with measurement without leaving the physical fragment.
  • First-order completeness means every completely-positive trace-preserving map on qubits is denotable by a closed term.
  • The same type discipline extends, without redesign, to a nonlinear fragment that admits recursion and controlled duplication (e.g., Repeat-Until-Success).

Where Pith is reading between the lines

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

  • The same static discipline could be used as a compilation target for higher-order quantum circuits that mix classical and quantum control of causal order.
  • Device references suggest a concrete intermediate representation for simulators that must keep superposed measurement outcomes consistent.
  • If the restriction on controllable branches can be relaxed while remaining inside Caus[CPM], the language would capture a still larger fragment of QC-QCs.

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

2 major / 4 minor

Summary. The paper defines a higher-order linear functional language for quantum processes with indefinite causal orders (ICOs), supporting general channels (not just unitaries) via a linear type system plus an extra discipline on the qcase construct (branches must be controllable terms of type A ⊸ q^n). It supplies a small-step operational semantics on configurations that uses device references and memory functions to synchronize measurement outcomes across superposed branches, a denotational semantics interpreting well-typed terms as morphisms of Caus[CPM], a soundness theorem equating the two semantics, first-order universality for all quantum channels, second-order universality for the subclass of QC-QCs with memory (containing the quantum switch), and a sketch of a nonlinear extension with recursion.

Significance. If the results hold, the work supplies the first programming language that faithfully realises the computational power of ICOs together with measurement, with physicality decidable statically in polynomial time by typing into Caus[CPM]. The operational-denotational soundness (Theorem 5.3), the constructive encodings of channels and of QC-QCs-with-memory, and the careful treatment of device references are genuine technical contributions that close a recognised gap left by both unitary-only linear calculi and nonlinear qcase languages. The appendices contain the remaining lemmas, giving a high degree of machine-checkable confidence in the linear fragment.

major comments (2)
  1. [§7 and App. F] Section 7 and Appendix F develop only the syntax and operational infrastructure of the nonlinear/recursive extension; subject reduction, progress and uniqueness of normal form are claimed to lift, but no denotational semantics in Caus[CPM] (or even CPM) and no soundness theorem are supplied. Because the abstract and introduction present the extension as a completed contribution, either the denotational account should be added or the claim should be explicitly limited to the operational level.
  2. [§6.2, Prop. 6.2, Rem. 6.3] Proposition 6.2 realises only the subclass of QC-QCs with memory (lists rather than sets in the control register). Remark 6.3 correctly flags the gap, yet the abstract and introduction speak of “a large subclass of \ldots QC-QCs, containing the quantum switch” without quantifying how large the subclass is relative to the full Wechs et al. hierarchy. A short paragraph comparing the two classes (or an explicit statement that general QC-QCs remain open) would prevent over-reading of the expressivity claim.
minor comments (4)
  1. [Props. 6.1 & 3.16] Proposition 6.1 title contains the typo “qantum”; Proposition 3.16 title contains “Uniqeness”.
  2. [§1.3.3, Fig. 2] Figure 2 caption and surrounding text refer to “QC-QCs” while the body sometimes writes “QC-QC”; a single expansion on first use would help readers unfamiliar with Wechs et al. 2021.
  3. [Fig. 7, qcase rule] In the operational rules (Fig. 7) the side-condition “t is fresh” for the qcase-value rule is never formalised; a one-line definition of freshness relative to free variables and device references would remove ambiguity.
  4. [§3.4] Appendix A.2–A.3 give detailed reductions that are helpful, yet the main text (Ex. 3.9, 3.11) only sketches them; a forward pointer would improve readability.

Circularity Check

0 steps flagged

No significant circularity: physicality is imported from the external Caus[CPM] construction; the language is shown to land inside it rather than defining the target by construction.

full rationale

The paper's strongest claims (well-typed terms denote morphisms of Caus[CPM], operational soundness Thm 5.3, FO universality Prop 6.1, SO universality for QC-QCs-with-memory Prop 6.2) do not reduce by construction to their own inputs. Physicality is obtained by interpreting the type system inside the pre-existing causal category of Kissinger & Uijlen (2019) and verifying that the denotational clauses (Fig. 10, Lem. 4.5, Prop. 4.6) produce morphisms of that category; the extra qcase discipline (branches controllable of type A ⊸ q^n) is an explicit restriction needed to stay inside Caus[CPM] (Remark 3.10 shows the naïve typing yields unphysical maps). Device references and memory functions are pure semantic bookkeeping for synchronizing measurement outcomes across superpositions; they are not fitted parameters. Expressivity results are constructive encodings (Stinespring + CNOT universality for channels; recursive encoding of the Wechs et al. circuit shape for QC-QCs-with-memory) rather than renamings of fitted data. The only self-citations are ordinary related-work pointers (e.g. Barsse et al. 2026 on vacuum-extended channels) and are not load-bearing for the main theorems. Score 1 reflects a single minor self-reference that does not force any central claim.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 2 invented entities

Pure theoretical CS/quantum-foundations paper. No numerical free parameters. Relies on standard categorical quantum mechanics (FHilb, CPM, compact closure, Caus construction) plus the domain assumption that linear control is the correct way to define coherent control on CP maps. The only invented semantic devices are device references and memory functions, introduced solely to make the small-step semantics well-defined.

axioms (3)
  • standard math FHilb and CPM are compact closed; the Caus construction of Kissinger & Uijlen yields a symmetric monoidal closed category whose morphisms are the physically meaningful higher-order maps.
    Invoked throughout Sections 4–5 to interpret types and prove that well-typed terms land in Caus[CPM].
  • domain assumption Coherent control of completely positive maps is well-defined precisely when the controlled processes share the same linear resources (the linear qcase).
    Stated in Remark 2.1 and used to justify the typing rule that forces identical free variables in both branches.
  • domain assumption Measurement outcomes occurring in distinct superposed branches that share a device reference must be identical.
    Operational motivation for device references and memory functions (Section 3.1–3.2).
invented entities (2)
  • Device references and memory functions no independent evidence
    purpose: Synchronise measurement outcomes across superposed branches of a qcase while remaining inside a linear operational semantics.
    Introduced purely as semantic bookkeeping; not claimed to be new physical objects.
  • Typing restriction that qcase branches must have type A ⊸ q^n and be controllable no independent evidence
    purpose: Exclude unphysical maps that would arise from a naïve tensor-product typing of qcase.
    Ad-hoc relative to pure linear logic, but justified by the Caus[CPM] requirement (Remark 3.10).

pith-pipeline@v1.1.0-grok45 · 51573 in / 2211 out tokens · 32326 ms · 2026-07-13T02:18:54.293345+00:00 · methodology

0 comments
read the original abstract

Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.

Figures

Figures reproduced from arXiv: 2607.09534 by Kathleen Barsse, Romain P\'echoux, Simon Perdrix.

Figure 1
Figure 1. Figure 1: (Left) The quantum switch program. (Right) A diagrammatic representation of the quantum switch. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The nested classes of supermaps defined in [ [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Syntax of the linear language for indefinite causal orders [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Typing rules. Recall that C is the set of controllable terms, i.e., those without measurements. Lastly, we define the set of controllable terms C ⊆ T as the set of terms that do not contain measurement. Controllable terms are the only ones that can appear in the branches of a qcase statement. This restriction is formalized by the type system in the following section. 2.2 Linear Type System The type system … view at source ↗
Figure 5
Figure 5. Figure 5: Syntax of execution terms typing rules are defined on terms of E : Δ ⊢ 𝑃 : q Δ ′ ⊢ 𝑀 : 𝐴 Δ ′ ⊢ 𝑁 : 𝐴 meas Δ, Δ ′ ⊢ meas 𝑑 ⊲ 𝑃 {0 → 𝑀 | 1 → 𝑁} : 𝐴 Δ ⊢ 𝑃 : q Δ ′ ⊢ 𝑀 : 𝐴 ⊸ q 𝑛 Δ ′ ⊢ 𝑁 : 𝐴 ⊸ q 𝑛 qcase Δ, Δ ′ ⊢ qcase 𝑃 {0 → 𝑀 | 1 → 𝑁} : 𝐴 ⊸ q 𝑛+1 Namely, the typing rule for measurement with a device reference is similar to the rule (meas) of [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Congruence relation ≡ 3.2.2 Adding Term Superpositions. In order to define the reduction rules, we must define linear combinations of terms. We define configurations, which allow term superpositions and are based on [Díaz-Caro, Guillermo, et al. 2019]’s notions of term distributions. The set of configurations, written as E®, is defined by the following grammar: (Configurations) E® ∋ 𝑀, ® 𝑁® ::= 0® | 𝑀𝜎 | 𝑀… view at source ↗
Figure 7
Figure 7. Figure 7: Reduction relation ↠ hypothesis 𝜎 ⊔ Mem(𝑀®) || Mem(𝑁®), which ensures that at each step of the reduction, the memory functions of each summand remain consistent. The hypothesis 𝑀𝜎 ∉ Supp(𝑁®) indicates that we are reducing one of the summands of the canonical form. This is to avoid artificially constructing an infinite derivation, for instance by starting with 𝑀 ≡ 1/2 · 𝑀 + 1/4 · 𝑀 + ... and reducing the fr… view at source ↗
Figure 8
Figure 8. Figure 8: Denotational semantics of controllable terms [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Extended syntax and only once. Indefinite causal order can thus be implemented when the state of memory register is in superposition. Each of these controlled open slot is intertwined with isometries 𝑉 →𝑘𝑛+1 | (𝑘1,...,𝑘𝑛 ) ⟩ that initialise and update the memory register in an appropriate way, depending on the higher order quantum operation one wants to implement.8 A more detailed presentation of QC-QCs wi… view at source ↗
Figure 10
Figure 10. Figure 10: Denotational semantics Lemma C.1. Let 𝑓 , 𝑔 : [Λ] → [𝐴 ⊸ q 𝑛 ] be morphisms of FHilb such that 𝐷(𝑓 ), 𝐷(𝑔) : JΛK → J𝐴 ⊸ q 𝑛 K are morphisms of Caus[CPM]. Then 𝐷(𝔮(𝑓 , 𝑔)) : JqK ⊗ JΛK → J𝐴 ⊸ q 𝑛+1 K is a morphism of Caus[CPM]. Proof. The proof relies on a few properties of causal categories. By [Kissinger and Uijlen 2019, Definition 5.1], the object JqK is first order. Since first-order systems are closed … view at source ↗
Figure 11
Figure 11. Figure 11: Denotational semantics of E Lemma 5.1. For all valid typing judgment Δ ⊢ 𝑀 : 𝐴 where 𝑀 ∈ E and valuation 𝜈 ∈ Ω+(𝑀), [Δ ⊢ 𝑀 : 𝐴]𝜈 is well defined. Proof. We show by induction on the derivation of Δ ⊢ 𝑀 : 𝐴 that its interpretation is indepen￾dent of the particular derivation of the typing judgment, similarly to the proof of Proposition 4.3. In particular, we use the fact that 𝜈 is also an extended valuation… view at source ↗
Figure 12
Figure 12. Figure 12: Typing rules (Extended execution terms) E ∗ ∋ 𝑀, 𝑁 , 𝑃 ::= 𝑥 | 𝑀𝑁 | 𝜆𝑥.𝑀 | 𝑢 | 𝑀∗𝑁 | 𝜆 ∗𝑢.𝑀 | ⟨𝑀, 𝑁⟩ | let ⟨𝑥, 𝑦⟩ = 𝑀 in 𝑁 | () | 𝑀; 𝑁 | 𝑈 | |0⟩ | |1⟩ | meas 𝑑 ∗ ⊲ 𝑃 {0 → 𝑀 | 1 → 𝑁} | qcase 𝑃 {0 → 𝑀 | 1 → 𝑁} | letrec 𝑓 𝑥 = 𝑀 | letrec∗ 𝑓 𝑢 = 𝑀 [PITH_FULL_IMAGE:figures/full_fig_p042_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Extended syntax of execution terms and the rules for all other primitives are the same as in T ∗ . In turn, the set of (extended) configurations, written as E®∗ is defined by the following grammar: (Extended configurations) E®∗ ∋ 𝑀, ® 𝑁® ::= 0® | 𝑀𝜎 | 𝑀® + 𝑁® | 𝛼 · 𝑀® where 𝑀 ∈ E ∗ , 𝛼 ∈ C and 𝜎 ∈ M∗ . F.2.2 Reduction Rules. To define the reduction of a term 𝑀 ∈ T ∗ , we assign to each measurement in 𝑀 a … view at source ↗
Figure 14
Figure 14. Figure 14: Reduction relation ↠ [PITH_FULL_IMAGE:figures/full_fig_p043_14.png] view at source ↗

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

52 extracted references · 18 canonical work pages · 2 internal anchors

  1. [1]

    Quantum query complexity of Boolean functions under indefinite causal order

    “Quantum query complexity of Boolean functions under indefinite causal order. ”Phys. Rev. Res., 6, 3, (July 2024), L032020. doi:10.1103/PhysRevResearch.6.L032020. Alastair A. Abbott, Julian Wechs, Dominic Horsman, Mehdi Mhalla, and Cyril Branciard

    work page doi:10.1103/physrevresearch.6.l032020 2024

  2. [2]

    John-Mark A

    doi:10.22331/Q-2020-09-24-333. John-Mark A. Allen, Jonathan Barrett, Dominic C. Horsman, Ciarán M. Lee, and Robert W. Spekkens. July

    work page doi:10.22331/q-2020-09-24-333 2020

  3. [3]

    Quantum Common Causes and Quantum Causal Models

    “Quantum Common Causes and Quantum Causal Models. ”Phys. Rev. X, 7, 3, (July 2017), 031021. doi:10.1103/PhysRevX.7.031021. Thorsten Altenkirch and Jonathan Grattage

    doi:10.1103/physrevx.7.031021 2017

  4. [4]

    doi:10.1109/LICS.2005.1

    IEEE Computer Society, 249–258. doi:10.1109/LICS.2005.1. Mateus Araújo, Fabio Costa, and Časlav Brukner. Dec

    doi:10.1109/lics.2005.1 2005

  5. [5]

    Computational Advantage from Quantum-Controlled Ordering of Gates

    “Computational Advantage from Quantum-Controlled Ordering of Gates. ”Phys. Rev. Lett., 113, (Dec. 2014), 250402, 25, (Dec. 2014). doi:10.1103/PhysRevLett.113.250402. Mateus Araújo, Philippe Allard Guérin, and Ämin Baumeler. Nov

    doi:10.1103/physrevlett.113.250402 2014

  6. [6]

    Quantum computation with indefinite causal structures

    “Quantum computation with indefinite causal structures. ”Phys. Rev. A, 96, 5, (Nov. 2017), 052315. doi:10.1103/PhysRevA.96.052315. Pablo Arrighi and Gilles Dowek

    doi:10.1103/physreva.96.052315 2017

  7. [7]

    Higher-Order Programs with Indefinite Causal Orders 27 Costin Bădescu and Prakash Panangaden

    doi:10.23638/LMCS-13(1:8)2017. Higher-Order Programs with Indefinite Causal Orders 27 Costin Bădescu and Prakash Panangaden

    doi:10.23638/lmcs-13(1:8)2017 2017

  8. [8]

    Quantum Alternation: Prospects and Problems

    “Quantum Alternation: Prospects and Problems. ” In:Proceedings of the 12th International Workshop on Quantum Physics and Logic, QPL 2015(EPTCS). Ed. by Chris Heunen, Peter Selinger, and Jamie Vicary, 33–42. doi:10.4204/EPTCS.195.3. Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. ...

    work page doi:10.4204/eptcs.195.3 2015

  9. [9]

    Elementary gates for quantum computation

    “Elementary gates for quantum computation. ”Phys. Rev. A, 52, (Nov. 1995), 3457–3467, 5, (Nov. 1995). doi:10.1103/PhysRevA.52.3457. Jonathan Barrett, Robin Lorenz, and Ognyan Oreshkov. 2019.Quantum Causal Models. (2019). arXiv: 1906.10726 [quant-ph]. Kathleen Barsse, Romain Péchoux, and Simon Perdrix. 2026.Quantum Control and General Recursion beyond the ...

    Pith/arXiv arXiv doi:10.1103/physreva.52.3457 1995

  10. [10]

    by Alastair F

    Ed. by Alastair F. Donaldson and Emina Torlak. Association for Computing Machinery, 286–300. doi:10.1145/3385412.3386007. Alessandro Bisio and Paolo Perinotti. May

    doi:10.1145/3385412.3386007

  11. [11]

    Theoretical framework for higher-order quantum theory

    “Theoretical framework for higher-order quantum theory. ”Proceedings. Mathematical, Physical, and Engineering Sciences, 475, 2225, (May 2019), 20180706. doi:10.1098/rspa.2018.0706. Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, and Thomas Vinet. 2026.Resource-A ware Quantum Programming with General Recursion and Quantum Control. (2026). arXiv: 2510.2...

    doi:10.1098/rspa.2018.0706 2019

  12. [12]

    Quantum computations without definite causal structure

    “Quantum computations without definite causal structure. ”Phys. Rev. A, 88, 2, (Aug. 2013), 022318. doi:10.1103/PhysRevA.88.022318. Man-Duen Choi

    doi:10.1103/physreva.88.022318 2013

  13. [13]

    Completely positive linear maps on complex matrices

    “Completely positive linear maps on complex matrices. ”Linear Algebra and its Applications, 10, 3, 285–290. doi:https://doi.org/10.1016/0024-3795(75)90075-0. Timoteo Colnaghi, Giacomo Mauro D’Ariano, Stefano Facchini, and Paolo Perinotti

    doi:10.1016/0024-3795(75)90075-0

  14. [14]

    Quantum computation with programmable connections between gates

    “Quantum computation with programmable connections between gates. ”Physics Letters A, 376, 45, 2940–2943. doi:https://doi.org/10.1016/j.physleta.20 12.08.028. Kinnari Dave, Louis Lemonnier, Romain Péchoux, and Vladimir Zamdzhiev

    doi:10.1016/j.physleta.20

  15. [15]

    Combining quantum and classical control: syntax, semantics and adequacy

    “Combining quantum and classical control: syntax, semantics and adequacy. ” In:Proceedings of the 28th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2025(Lecture Notes in Computer Science). Ed. by Parosh Aziz Abdulla and Delia Kesner. Springer, 155–175. doi:10.1007/978-3-031-90897-2_8. Alejandro Díaz-Caro ...

    doi:10.1007/978-3-031-90897-2_8 2025

  16. [16]

    Typing Quantum Superpositions and Measurement

    “Typing Quantum Superpositions and Measurement. ” In:Proceedings of the 6th International Conference on Theory and Practice of Natural Computing, TPNC 2017(Lecture Notes in Computer Science). Ed. by Carlos Martín-Vide, Roman Neruda, and Miguel A. Vega-Rodríguez. Springer, 281–293. doi:10.1007/978-3-319-710 69-3_22. Alejandro Díaz-Caro, Gilles Dowek, and J...

    work page doi:10.1007/978-3-319-710 2017

  17. [17]

    Two linearities for quantum computing in the lambda calculus

    “Two linearities for quantum computing in the lambda calculus. ”Biosyst., 186, 104012. doi:10.1016/J.BIOSYSTEMS.2019.104012. Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron

    work page doi:10.1016/j.biosystems.2019.104012 2019

  18. [18]

    doi:10.1109/LICS.2019.8785834

    IEEE, 1–13. doi:10.1109/LICS.2019.8785834. Alejandro Díaz-Caro and Octavio Malherbe

    work page doi:10.1109/lics.2019.8785834 2019

  19. [19]

    Daniel Ebler, Sina Salek, and Giulio Chiribella

    doi:10.46298/LMCS-18(3:32)2022. Daniel Ebler, Sina Salek, and Giulio Chiribella. Mar

    work page doi:10.46298/lmcs-18(3:32)2022 2022

  20. [20]

    Enhanced Communication with the Assistance of Indefinite Causal Order

    “Enhanced Communication with the Assistance of Indefinite Causal Order. ”Phys. Rev. Lett., 120, 12, (Mar. 2018), 120502. doi:10.1103/PhysRevLett.120.120502. Stefano Facchini and Simon Perdrix

    doi:10.1103/physrevlett.120.120502 2018

  21. [21]

    Quantum Circuits for the Unitary Permutation Problem

    “Quantum Circuits for the Unitary Permutation Problem. ” In:Proceedings of the 12th Annual Conference on Theory and Applications of Models of Computation, TAMC 2015(Lecture Notes in Computer Science). Ed. by Rahul Jain, Sanjay Jain, and Frank Stephan. Springer, 324–331. doi:10.1007/978-3-319-17142-5_28. Jean-Yves Girard

    work page doi:10.1007/978-3-319-17142-5_28 2015

  22. [22]

    Linear Logic

    “Linear Logic. ”Theor. Comput. Sci., 50, 1–102. doi:10.1016/0304-3975(87)90045-4. Lov K. Grover

    doi:10.1016/0304-3975(87)90045-4

  23. [23]

    A fast quantum mechanical algorithm for database search

    “A fast quantum mechanical algorithm for database search. ” In:Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing(STOC ’96). Association for Computing Machinery, Philadelphia, Pennsylvania, USA, 212–219.isbn: 0897917855. doi:10.1145/237814.237866. Chris Heunen, Louis Lemonnier, Christopher McNally, and Alex Rice

    doi:10.1145/237814.237866

  24. [24]

    Quantum Circuits Are Just a Phase

    “Quantum Circuits Are Just a Phase. ”Proc. ACM Program. Lang., 10, POPL, 2586–2613. doi:10.1145/3776731. Timothée Hoffreumon and Ognyan Oreshkov. Jan

    work page doi:10.1145/3776731

  25. [25]

    Projective characterization of higher-order quantum transforma- tions

    “Projective characterization of higher-order quantum transforma- tions. ”Quantum, 10, (Jan. 2026),

    2026

  26. [26]

    doi:10.22331/q-2026-01-21-1978. A. Jamiołkowski

    work page doi:10.22331/q-2026-01-21-1978 2026

  27. [27]

    Linear transformations which preserve trace and positive semidefiniteness of operators

    “Linear transformations which preserve trace and positive semidefiniteness of operators. ”Reports on Mathematical Physics, 3, 4, 275–278. doi:https://doi.org/10.1016/0034-4877(72)90011-0. Anna Jenčová. May

    doi:10.1016/0034-4877(72)90011-0

  28. [28]

    On the structure of higher order quantum maps

    “On the structure of higher order quantum maps. ”Quantum, 10, (May 2026),

    2026

  29. [29]

    28 Kathleen Barsse, Romain Péchoux, and Simon Perdrix G.M

    doi:10.22331/q- 2026-05-05-2090. 28 Kathleen Barsse, Romain Péchoux, and Simon Perdrix G.M. Kelly and M.L. Laplaza

    doi:10.22331/q- 2026

  30. [30]

    Coherence for compact closed categories

    “Coherence for compact closed categories. ”Journal of Pure and Applied Algebra, 19, 193–213. doi:https://doi.org/10.1016/0022-4049(80)90101-2. Aleks Kissinger and Sander Uijlen

    doi:10.1016/0022-4049(80)90101-2

  31. [31]

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

    doi:10.23638/LMCS-15(3:15)2019. Hlér Kristjánsson, Tatsuki Odake, Satoshi Yoshida, Philip Taranto, Jessica Bavaresco, Marco Túlio Quintino, and Mio Murao. 2024.Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits. (2024). arXiv: 2409.18420[quant-ph]. Saunders Mac Lane. 1971.Cat...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.23638/lmcs-15(3:15)2019 2019

  32. [32]

    Adam Paetznick and Krysta M

    doi:10.1038/ncomms2076. Adam Paetznick and Krysta M. Svore

    doi:10.1038/ncomms2076

  33. [33]

    Repeat-until-success: non-deterministic decomposition of single-qubit unitaries

    “Repeat-until-success: non-deterministic decomposition of single-qubit unitaries. ” Quantum Inf. Comput., 14, 15-16, 1277–1301. doi:10.26421/QIC14.15-16-2. Martin J Renner and Časlav Brukner. June

    doi:10.26421/qic14.15-16-2

  34. [34]

    Computational Advantage from a Quantum Superposition of Qubit Gate Orders

    “Computational Advantage from a Quantum Superposition of Qubit Gate Orders. ”Phys. Rev. Lett., 128, 23, (June 2022), 230503. doi:10.1103/PhysRevLett.128.230503. Martin J Renner and Časlav Brukner. Oct

    work page doi:10.1103/physrevlett.128.230503 2022

  35. [35]

    Reassessing the computational advantage of quantum-controlled ordering of gates

    “Reassessing the computational advantage of quantum-controlled ordering of gates. ”Phys. Rev. Res., 3, (Oct. 2021), 043012, 4, (Oct. 2021). doi:10.1103/PhysRevResearch.3.043012. Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto

    work page doi:10.1103/physrevresearch.3.043012 2021

  36. [36]

    From Symmetric Pattern-Matching to Quantum Control

    “From Symmetric Pattern-Matching to Quantum Control. ” In: Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2018(Lecture Notes in Computer Science). Ed. by Christel Baier and Ugo Dal Lago. Springer, 348–364. doi:10.1007/978-3- 319-89366-2_19. Peter Selinger

    doi:10.1007/978-3- 2018

  37. [37]

    Towards a quantum programming language

    “Towards a quantum programming language. ”Mathematical Structures in Computer Science, 14, 4, 527–586. doi:10.1017/S0960129504004256. W. Forrest Stinespring

    doi:10.1017/s0960129504004256

  38. [38]

    Positive Functions on C*-Algebras

    “Positive Functions on C*-Algebras. ”Proceedings of the American Mathematical Society, 6, 2, 211–216. doi:10.1090/S0002-9939-1955-0069403-4. Márcio M. Taddei et al.. Feb

    doi:10.1090/s0002-9939-1955-0069403-4 1955

  39. [39]

    Computational Advantage from the Quantum Superposition of Multiple Temporal Orders of Photonic Gates

    “Computational Advantage from the Quantum Superposition of Multiple Temporal Orders of Photonic Gates. ”PRX Quantum, 2, 1, (Feb. 2021), 010320. doi:10.1103/PRXQuantum.2.010320. Takeshi Tsukada and Kazuyuki Asada

    doi:10.1103/prxquantum.2.010320 2021

  40. [40]

    Enriched Presheaf Model of Quantum FPC

    “Enriched Presheaf Model of Quantum FPC. ”Proc. ACM Program. Lang., 8, POPL, 362–392. doi:10.1145/3632855. Benoît Valiron

    work page doi:10.1145/3632855

  41. [41]

    Semantics of quantum programming languages: Classical control, quantum control

    “Semantics of quantum programming languages: Classical control, quantum control. ”Journal of Logical and Algebraic Methods in Programming, 128, 100790. doi:10.1016/j.jlamp.2022.100790. André van Tonder

    work page doi:10.1016/j.jlamp.2022.100790 2022

  42. [42]

    A Lambda Calculus for Quantum Computation

    “A Lambda Calculus for Quantum Computation. ”SIAM J. Comput., 33, 5, 1109–1135. doi:10.1137/S0 097539703432165. Augustin Vanrietvelde, Nick Ormrod, Hlér Kristjánsson, and Jonathan Barrett. Dec

    work page doi:10.1137/s0

  43. [43]

    Consistent circuits for indefinite causal order

    “Consistent circuits for indefinite causal order. ”Quantum, 9, (Dec. 2025),

    2025

  44. [44]

    Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks

    doi:10.22331/q-2025-12-02-1923. Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks

    work page doi:10.22331/q-2025-12-02-1923 2025

  45. [45]

    Qunity: A Unified Language for Quantum and Classical Computing

    “Qunity: A Unified Language for Quantum and Classical Computing. ”Proc. ACM Program. Lang., 7, POPL, 921–951. doi:10.1145/3571225. Julian Wechs, Hippolyte Dourdent, Alastair A. Abbott, and Cyril Branciard. Aug

    doi:10.1145/3571225

  46. [46]

    Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs

    “Quantum Circuits with Classical Versus Quantum Control of Causal Order. ”PRX Quantum, 2, 3, (Aug. 2021), 030335. doi:10.1103/PRXQuantum.2.030335. Mingsheng Ying, Nengkun Yu, and Yuan Feng. 2014.Alternation in quantum programming: from superposition of data to superposition of programs. (2014). arXiv: 1402.5172[cs.PL]. Mingsheng Ying, Nengkun Yu, and Yuan...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1103/prxquantum.2.030335 2021

  47. [47]

    Verification of recursively defined quantum circuits

    “Verification of recursively defined quantum circuits. ” In:Conference on Programming Language Design and Implementation (PLDI). arXiv: 2404.05934[quant-ph]. Charles Yuan, Agnes Villanyi, and Michael Carbin

    Pith/arXiv arXiv

  48. [48]

    Quantum Control Machine: The Limits of Control Flow in Quantum Programming

    “Quantum Control Machine: The Limits of Control Flow in Quantum Programming. ”Proc. ACM Program. Lang., 8, OOPSLA1, 1–28. doi:10.1145/3649811. Zhicheng Zhang and Mingsheng Ying

    doi:10.1145/3649811

  49. [49]

    Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs

    “Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs. ”Proc. ACM Program. Lang., 9, PLDI, 822–847. doi:10.1145/3729283. Higher-Order Programs with Indefinite Causal Orders 29 Appendices A Additional Details on Examples A.1 Typing Derivations for Section 2.3 Here, we give the typing derivations for the examples of Section 2.3. ...

    doi:10.1145/3729283

  50. [50]

    Then 𝐷(𝔮(𝑓 , 𝑔)) : JqK⊗JΛK→J𝐴⊸q 𝑛+1K is a morphism ofCaus[CPM]

    Denotational semantics Lemma C.1.Let 𝑓 , 𝑔 : [Λ] → [𝐴⊸q 𝑛] be morphisms of FHilb such that 𝐷(𝑓), 𝐷(𝑔) : JΛK→ J𝐴⊸q 𝑛K are morphisms of Caus[CPM] . Then 𝐷(𝔮(𝑓 , 𝑔)) : JqK⊗JΛK→J𝐴⊸q 𝑛+1K is a morphism ofCaus[CPM]. Proof. The proof relies on a few properties of causal categories. By [Kissinger and Uijlen 2019, Definition 5.1], the object JqK is first order. Si...

    2019

  51. [51]

    Then the result follows from [Kissinger and Uijlen 2019, Lemma 4.9], using the fact that for all 𝜌∈𝑐 JqK,𝑇 𝑟(𝑈 𝜌𝑈 †)=1

    and 𝑐JqK∗ ={𝑇 𝑟} . Then the result follows from [Kissinger and Uijlen 2019, Lemma 4.9], using the fact that for all 𝜌∈𝑐 JqK,𝑇 𝑟(𝑈 𝜌𝑈 †)=1. For the qcase rule, the statement follows from Lemma C.1.□ Proposition 4.6.The interpretationJ·Kis well defined. Proof. To prove that the interpretation is well defined, we show that the interpretation of each valid ty...

    2019

  52. [52]

    Denotational semantics ofE Lemma 5.1.For all valid typing judgment Δ⊢𝑀 : 𝐴 where 𝑀∈E and valuation 𝜈∈Ω +(𝑀) , [Δ⊢𝑀:𝐴] 𝜈 is well defined. Proof. We show by induction on the derivation of Δ⊢𝑀 : 𝐴 that its interpretation is indepen- dent of the particular derivation of the typing judgment, similarly to the proof of Proposition 4.3. In particular, we use the ...

    1955