Pith. sign in

REVIEW 2 major objections 6 minor 43 references

Quantalic lambda-calculus and additive disjunction

T0 review · 2 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read The paper extends quantalic linear lambda-calculus with additive disjunction and proves the resulting (in)equational system sound for enriched co-Cartesian autonomous categories and approximately complete over continuous quantales.

desk verdict Genuinely new additive disjunction for quantalic lambda-calculus with solid model constructions, but the central soundness and approximate-completeness proofs are sketches that need to be written out before I would trust them. read the letter →

arxiv 2608.06120 v1 pith:DQWRDNRF submitted 2026-08-06 cs.LO math.CT

Renato Neves , Bruna Salgado This is my paper · ORCID
classification cs.LOmath.CT MSC 03B7003F5218D2068Q55
keywords quantaliclambda-calculusadditivedisjunctioncasestatementsquantaleapproximatecompletenessenrichedcategorytheorygeneralisedmetricspacesprobabilisticprogramming
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper extends quantalic linear $\lambda$-calculus — an equational system in which every (in)equation $\Gamma \vdash t \leq_q s$ is labelled by an element $q$ of a quantale, so that the label behaves like a distance between terms — with additive disjunction $\oplus$, the type constructor that gives case statements. Its main results are soundness and approximate completeness: the extended system is sound for $\mathcal{V}$-Cat-separated co-Cartesian autonomous categories (categories whose morphism sets are separated $\mathcal{V}$-categories and whose coproducts respect the product enrichment), and over continuous quantales any (in)equation true in all models is provable at every sufficiently close approximation $r \ll q$ of its label $q$. The new congruence rule for case statements compounds labels as $p \otimes (q \wedge r)$, a worst-case combination of the test's distance and the two branch distances. The paper exhibits models based on generalised metric spaces, gluing, enriched presheaves, Banach spaces, and a Karoubi envelope of quantum channels, and uses the Banach-space model to justify reasoning about Cauchy sequences of random walks.

What carries the argument

The central object is the quantale $\mathcal{V}$ with its way-below relation $\ll$, together with the new congruence rule for case statements at the bottom of Figure 3. That rule states that from $t \leq_p s$, $u \leq_q v$, and $w \leq_r o$ one may infer $\mathrm{case}\, t\{ \ldots \} \leq_{p \otimes (q \wedge r)} \mathrm{case}\, s\{ \ldots \}$; the label $p \otimes (q \wedge r)$ encodes a worst-case assumption, since the branch whose terms differ more is controlled by the smaller of $q$ and $r$, compounded with the distance $p$ between the tested terms. The other load-bearing piece is the basis $B$ of the continuous lattice: hom-objects of the syntactic category $\mathrm{Syn}(T)$ are formed by taking suprema over labels $q$ for which $t \leq_q s$ is a theorem, and rule (join) keeps those sets directed, so an approximation $r \ll q$ can be extracted as a finite join of theorems. Continuity of $\mathcal{V}$ enters through the preservation of directed suprema by $q \wedge (-)$, which makes the coproducts of $\mathrm{Syn}(T)$ enriched over products.

What would settle it

Check the proof of Theorem 3.13 at the step where coproduct enrichment in Syn(T) is proved: compute whether sup{q∧r : q∈Q, r∈R} equals (sup Q)∧(sup R) for directed sets Q,R of labels. This identity is exactly what continuity supplies via q∧(−), so a non-continuous quantale where it fails would show approximate completeness cannot extend beyond the stated continuity assumption.

Watch

Extended reading notes

Core claim

The central claim is that the quantalic (in)equational system obtained by adding additive disjunction to quantalic linear $\lambda$-calculus is sound and approximately complete: Theorem 3.12 states that every provable inequation is satisfied in every model, and Theorem 3.13 states that over a continuous quantale, if $\Gamma \vdash t \leq_q s$ holds in all models of a $\mathcal{V}\lambda$-theory $T$, then for every basis element $r \ll q$ the inequation $\Gamma \vdash t \leq_r s$ is a theorem of $T$. This recovers ordinary completeness when $q$ is compact, and it deliberately avoids the Archimedean rule, which involves infinitely many premisses. The proof builds a syntactic category $\mathrm{Syn}(T)$ whose hom-objects are separated $\mathcal{V}$-categories of terms, shows its coproducts are enriched over products using the distributivity of $q \wedge (-)$ over directed suprema, and then uses the way-below relation together with the (join) rule to extract a finite join of theorems from semantic validity.

Load-bearing premise

The load-bearing premise is that the quantale's underlying lattice is continuous, so that intersecting with any fixed label preserves directed unions.

Editorial extensions

If this is right

  • Quantitative extensionality for disjunctive types becomes a theorem: if $t$ restricted to the left injection is within $q$ of $s$, and $t$ restricted to the right injection is within $r$ of $s$, then the unrestricted terms are within $q \wedge r$.
  • Over the metric quantale, semantic verification of an approximation can be converted into syntactic proofs up to arbitrary rational precision, because the extended non-negative rationals form a basis of the quantale.
  • The gluing construction extends to the enriched quantalic setting, enabling categorical study of meta-theoretic properties such as conservativity and concrete completeness for the extended calculus.
  • In the Banach-space model, perturbations of predicates or actions propagate to $k$-step random walks with explicit metric bounds, so the calculus supports certified approximations of probabilistic programs.
  • In the quantum setting, the Karoubi envelope of quantum channels supplies the missing coproducts, so conditionals and higher-order structure coexist in a metric-enriched model.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural testable extension the paper leaves implicit is additive conjunction $\&$: the same enriched-coproduct machinery should dualize to products, with the worst-case label presumably flipping from $q \wedge r$ to $q \vee r$, though the paper does not prove this.
  • The $p \otimes (q \wedge r)$ rule is a template for quantitative case analysis beyond lambda-calculus: any deductive system whose labels form a continuous quantale could adopt the same rule and inherit approximate completeness, provided its syntactic category supports a directed join of premises.
  • The quantum model suggests a metric treatment of measurement as a conditional: once idempotents are split via the Karoubi envelope, a qubit measurement type $2 \to 1 + 1$ becomes representable, and the paper's random-walk approximation technique could be repeated for quantum walks with distance bounds given by the diamond norm.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 6 minor

Summary. This paper extends the quantalic linear lambda-calculus of [DN22, DN23b] with additive disjunction and case statements. It adds a quantalic (in)equational system (Figure 3), defines V-Cat-co-Cartesian autonomous categories as the semantic setting, and claims soundness (Theorem 3.12) and approximate completeness over continuous quantales (Theorem 3.13). The paper also presents several classes of models, including generalized metric spaces, gluing, enriched presheaves, Banach spaces, and a Karoubi-envelope category of quantum channels, and illustrates the framework on quantitative reasoning about random walks.

Significance. If the central proofs are completed, this is a worthwhile contribution: it gives a finitary quantitative axiomatization of additive disjunction, an approximate-completeness result that avoids the Archimedean rule, and several nontrivial models with potential applications in probabilistic and quantum programming. The Lindenbaum-Tarski strategy is standard and non-circular, and the continuity assumption on the quantale is used in a principled way. The Banach-space and quantum-channel constructions are concrete and give useful evidence that the notion of model is not vacuous. However, the current manuscript leaves two load-bearing verification steps at the level of assertion, so the advertised soundness and approximate-completeness results are not yet fully established.

major comments (2)
  1. [§3.3 (Theorem 3.13, Step 2)] The proof that Syn(T) is a V-Cat^sep-co-Cartesian model of T is incomplete. The displayed chain in Step 2 verifies only the inequality a(t,t')∧a(s,s') ≤ a([t,s],[t',s']), i.e. the V-functor condition for the co-pairing map in Eq. (2). It does not verify that this map is well defined on the separated quotient, that the injections are V-functors, that the type A⊕B together with the injections and case elimination satisfies the enriched universal property, or that the final rule of Figure 3 is sound in an arbitrary V-Cat-co-Cartesian autonomous category, including non-integral quantales. Moreover, the displayed derivation needs an explicit use of the case rule with the unit label k to obtain [t,s]≤_{q∧r}[t',s'] and then the weak rule to pass to q; this step is absent. Since Syn(T) is the only model used to derive approximate completeness, this is a load-bearing gap.
  2. [§3.3 (Theorem 3.12)] Soundness is asserted with the one-line proof 'follows straightforwardly by induction'. The new case rule in Figure 3, whose label is p⊗(q∧r), must be justified by a chain through enriched composition, enriched tensor, the V-functor property of co-pairing (Eq. (2)), and the distributivity isomorphism in a co-Cartesian autonomous category. No such chain is supplied. This matters not only for Theorem 3.12 itself but also for Theorem 3.13, because the same rule is used in the construction of the syntactic model. The reader is left without a verification of a central claim of the paper.
minor comments (6)
  1. [§3.3, Step 2 notation] The substitutions t[z/a] and s[w/b] are not consistent with the free-variable conventions used in Eq. (4), where a common fresh variable is substituted into two single-variable judgments; please rewrite this part with clear variables, for example t[z/x] and s[z/y], and avoid reusing a and b both as term names and as variable names.
  2. [§2.2, Example 2.3] There is a typo: 'The latter is also a a basis' should read 'a basis'.
  3. [§3.2, Definition 3.9] 'A Vλ-theory ((G,Σ), Ax) is a triple' should be 'is a pair' or 'is data consisting of'; there are only two components displayed.
  4. [§4.1] The diagram of reflections and adjunctions involving V-Cat, V-Cat^sep, V-Cat^sym, and V-Cat^{sym,sep} is garbled in the text and should be redrawn with explicit functor directions and labels.
  5. [§5.1, Example 5.2] The displayed limit line contains 'µ(-∞, q_n)' without the interval; it should read µ((-∞,q_n)). Also, 'linearcontractions' in §5.1 is missing a space.
  6. [Title] The running title 'QUANT ALIC' appears to be a misspelling of 'QUANTALIC'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the approximate-completeness proof is a standard term-model argument and the same-author citations are independent, peer-reviewed base results.

full rationale

The central derivation chain (Theorem 3.12 soundness and Theorem 3.13 approximate completeness) is not circular. Theorem 3.13 uses the standard Lindenbaum-Tarski construction: Syn(T) has hom-distances defined as suprema of provable labels (Eq. 4), and Step (3) shows that if q≤a(t,s) then every r≪q is a theorem via the way-below property and the (join)/(weak) rules. This is the normal completeness direction: satisfaction in Syn(T) is derived from the definition of the distance plus the deductive rules, not assumed to be the theoremhood conclusion. Step (2) proves the co-pairing enrichment inequality a(t,t')∧a(s,s')≤a([t,s],[t',s']) from the V-congruence rules of Figure 3; this is exactly the required V-functor condition being established for Syn(T), not imported as a premise. The proof is abbreviated (well-definedness on the separated quotient and the full enriched universal property are not written out), but that is a verification gap, not a circular reduction. The paper leans on [DN22, DN23b] for the multiplicative base, the autonomous structure of Syn(T), and the enrichment of Ban and CPTP; these are peer-reviewed same-author results that do not contain the additive-disjunction target, so under the review rules they count as independent support rather than circularity. There are no fitted parameters relabelled as predictions, and no equation in the paper reduces the claimed theorem to its own input by construction.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The general calculus has no fitted numerical constants; the applications use arbitrary inputs (q_n, delta, epsilon) that are given, not fitted to make the theorems true. No new physical or mathematical entities are postulated; the framework is built from existing structures such as quantales, V-categories, and Karoubi envelopes.

assumptions (5)
  • domain assumption The underlying lattice L of V is continuous and has a basis B closed under finite joins, binary meets, the unit k, and the multiplication of the quantale.
    Stated in Section 2.2 before Example 2.3. Theorem 3.13 and the enrichment of coproducts in Syn(T) depend on q∧(-) preserving directed suprema, which comes from continuity.
  • ad hoc to paper A model must be a V-Cat-co-Cartesian autonomous category, meaning binary coproducts are enriched over the Cartesian structure of V-Cat via a V-functor co-pairing.
    Definition 3.8 and equation (2). This is the new semantic condition introduced to make the additive-disjunction rules sound; it is natural but is chosen to match the syntax.
  • domain assumption The enriched presheaf model assumes the tensor of C distributes over binary coproducts.
    Section 4.3 uses this to show the exponential in [C^op,V-Cat-sep] restricts to finite-product preserving presheaves.
  • ad hoc to paper The random-walk application postulates that (p_qn(m(*)))_n is Cauchy and converges to p_{sqrt(2)/2}(m(*)), equation (5).
    These axioms are part of the example theory, not the general calculus; the paper verifies them semantically in Ban, so they are not hidden inputs to the main theorems.
  • standard math Standard external results: Day's reflection theorem, Kraus representation theorem, diamond-norm identities, and [GHK+03] facts on continuous lattices.
    Imported in Sections 4.3 and 5.2. These are established results and do not depend on the paper's claims.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Quantalic lambda-calculus and additive disjunction." pith.science (2026). https://pith.science/paper/DQWRDNRF

@misc{pith2026260806120,
  author       = {Pith},
  title        = {Pith review of: Quantalic lambda-calculus and additive disjunction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DQWRDNRF}},
  note         = {Machine review of arXiv:2608.06120}
}
read the original abstract

Motivated by the need to reason about case statements quantitatively, we extend quantalic linear lambda-calculus with additive disjunction. We show that the resulting equational system is sound. We also show that when certain continuity properties (of the underlying quantale) are adopted, it is additionally (approximately) complete. We present several models of the extended calculus, involving for example meta-theoretical properties in categorical logic (gluing), probabilistic, and quantum computation. As a concrete application, we illustrate how a probabilistic model, based on Banach spaces, can be synergistically used with the calculus' equational system to reason about Cauchy sequences of random walks. This highlights the emergent shift from "program semantics as the science of program equivalence" to flexible, quantitative perspectives, involving functional analysis and beyond.

Figures

Figures reproduced from arXiv: 2608.06120 by the authors.

Figure 1
Figure 1. Judgement formation rules of quantalic linear λ-calculus with additive disjunction. The extended calculus inherits desirable features from the original calculus [DN22, DN23b]. Most notably it inherits the unique derivation, substitution, and exchange properties, which rely on the aforementioned shuffling mechanism and Church’s typing style. Theorem 2.1. The judgement formation rules in [PITH_FULL_IMAGE:figures/full… view at source ↗
Figure 2
Figure 2. Syntactic axiomatics of co-Cartesian autonomous categories. We will assume that the underlying lattice L of V is continuous and has a basis B closed under finite joins, binary meets, the unit k and the multiplication ⊗ of the quantale. Example 2.3. The Boolean quantale (L := ({0 ≤ 1}, ∨), ⊗ := ∧, k := ⊤) is finite and thus satisfies the conditions above [GHK+03]. More generally, every coherent locale satisfies these… view at source ↗
Figure 3
Figure 3. The quantalic (in)equational system. Example 2.5. We conclude the section by briefly illustrating quantitative reasoning via the quantalic system that was just presented. Specifically we involve the notion of extensionality relative to disjunctive types: in the classical setting, strict equality between two (higher-order) terms t, s : A1 ⊕ A2 ⊸ B is entailed by the two equalities below. ( x : A1 ▷ t (inl(x)) = s (in… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Interpretation rules of quantalic linear λ-calculus with additive disjunction. Lemma 3.1 (Exchange and Substitution). For all judgements Γ, x : A, y : B, ∆ ▷ t : C, Γ, x : A ▷ s : B, and ∆ ▷ w : A, the following equations hold in every co-Cartesian autonomous category …
Figure 5
Figure 5. Figure 5: V-axiomatic schema of the presheaf P (above dotted line) and the V-(in)equational system of multi-sorted universal algebra (below the dotted line). Indeed, the fact that the first and second equation must hold is direct. As for the third equation, observe that due to n…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    Aliprantis and Kim C

    Charalambos D. Aliprantis and Kim C. Border. Infinite Dimensional Analysis: A Hitchhiker's Guide . Springer, Berlin, 3rd edition, 2006

    work page 2006

  2. [2]

    Strecker

    Ji r \' Ad \' a mek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories - The Joy of Cats . Dover Publications, 2009

    work page 2009

  3. [3]

    Locally Presentable and Accessible Categories , volume 189 of London Mathematical Society Lecture Note Series

    Ji r \' i Ad\' a mek and Ji r \' i Rosick\' y . Locally Presentable and Accessible Categories , volume 189 of London Mathematical Society Lecture Note Series . Cambridge University Press, Cambridge, 2009

    work page 2009

  4. [4]

    How nice are free completions of categories? Topology and its Applications , 273, 2020

    Ji r \' Ad \'a mek and Ji r \' Rosick \`y . How nice are free completions of categories? Topology and its Applications , 273, 2020

    work page 2020

  5. [5]

    Foundations of Probabilistic Programming

    Gilles Barthe, Joost - Pieter Katoen, and Alexandra Silva, editors. Foundations of Probabilistic Programming . Cambridge University Press, 2020

    work page 2020

  6. [6]

    Handbook of categorical algebra: Categories and structures , volume 2

    Francis Borceux. Handbook of categorical algebra: Categories and structures , volume 2. Cambridge University Press, 2009

    work page 2009

  7. [7]

    Functional Analysis in Asymmetric Normed Spaces

    S tefan Cobza s . Functional Analysis in Asymmetric Normed Spaces . Frontiers in Mathematics. Birkh \"a user Basel, Basel, 2013

    work page 2013

  8. [8]

    Roy L. Crole. Categories for Types . Cambridge mathematical textbooks. Cambridge University Press, 1993

    work page 1993

Show all 43 references
  1. [9]

    A reflection theorem for closed categories

    Brian Day. A reflection theorem for closed categories. Journal of Pure and Applied Algebra , 2(1):1--11, 1972

    1972

  2. [10]

    Semantics of higher-order probabilistic programs with conditioning

    Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Proc. ACM Program. Lang. , 4( POPL ):57:1--57:29, 2020

    2020

  3. [11]

    o ttingen, Germany (Virtual Conference), February 14-19, 2022 , volume 216 of LIPIcs , pages 16:1--16:18. Schloss Dagstuhl - Leibniz-Zentrum f \

    Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, G \" o ttingen, Germany (Virtual Conference), February ...

    2022

  4. [12]

    A complete v-equational system for graded lambda-calculus

    Fredrik Dahlqvist and Renato Neves. A complete v-equational system for graded lambda-calculus. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomingto...

    2023

  5. [13]

    The syntactic side of autonomous categories enriched over generalised metric spaces

    Fredrik Dahlqvist and Renato Neves. The syntactic side of autonomous categories enriched over generalised metric spaces. Log. Methods Comput. Sci. , 19(4), 2023

    2023

  6. [14]

    Fixed point logics on hemimetric spaces

    David Fern \'a ndez-Duque and Quentin Gougeon. Fixed point logics on hemimetric spaces. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--13, Boston, MA, USA, 2023. IEEE

    2023

  7. [15]

    Ross, and Peter Selinger

    Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. On the lambek embedding and the category of product-preserving presheaves. CoRR , abs/2205.06068, 2022

    2022 arXiv

  8. [16]

    Lawson, Michael Mislove, and Dana S

    Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott. Continuous Lattices and Domains , volume 93 of Encyclopedia of Mathematics and its Applications . Cambridge University Press, Cambridge, 2003

    2003

  9. [17]

    Categorical glueing and logical predicates for models of linear logic

    Masahito Hasegawa. Categorical glueing and logical predicates for models of linear logic. Technical report, January 1999

    1999

  10. [18]

    Logical predicates for intuitionistic linear type theories

    Masahito Hasegawa. Logical predicates for intuitionistic linear type theories. In Jean - Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings , volume 1581 of Lecture Notes in Computer ...

    1999

  11. [19]

    Completely positive projections and biproducts

    Chris Heunen, Aleks Kissinger, and Peter Selinger. Completely positive projections and biproducts. 171:71--83, 2014

    2014

  12. [20]

    Glueing and orthogonality for models of linear logic

    Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theor. Comput. Sci. , 294(1/2):183--231, 2003

    2003

  13. [21]

    Seal, and Walter Tholen, editors

    Dirk Hofmann, Gavin J. Seal, and Walter Tholen, editors. Monoidal Topology: A Categorical Approach to Order, Metric, and Topology , volume 153 of Encyclopedia of Mathematics and its Applications . Cambridge University Press, Cambridge, 2014

    2014

  14. [22]

    Categorical Logic and Type Theory , volume 141 of Studies in Logic and the Foundations of Mathematics

    Bart Jacobs. Categorical Logic and Type Theory , volume 141 of Studies in Logic and the Foundations of Mathematics . Elsevier, Amsterdam, 1999

    1999

  15. [23]

    Algebraic reasoning over relational structures

    Jan Jurka, Stefan Milius, and Henning Urbat. Algebraic reasoning over relational structures. CoRR , abs/2401.08445, 2024

    2024 arXiv

  16. [24]

    Johnstone

    Peter T. Johnstone. Stone Spaces , volume 3 of Cambridge Studies in Advanced Mathematics . Cambridge University Press, 1982

    1982

  17. [25]

    Sketches of an Elephant -- A Topos Theory Compendium , volume 2 of Oxford Logic Guides

    Peter Johnstone. Sketches of an Elephant -- A Topos Theory Compendium , volume 2 of Oxford Logic Guides . Oxford University Press, 2002

    2002

  18. [26]

    G. M. Kelly. Basic Concepts of Enriched Category Theory , volume 64 of London Mathematical Society Lecture Note Series . Cambridge University Press, Cambridge, 1982

    1982

  19. [27]

    Logiques, Categories et Machines: Implantation de Langages de Programmation guid \'e e par la Logique Cat \'e gorique

    Yves Lafont. Logiques, Categories et Machines: Implantation de Langages de Programmation guid \'e e par la Logique Cat \'e gorique . PhD thesis, Universite Paris VII, 1988

    1988

  20. [28]

    On quantitative algebraic higher-order theories

    Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On quantitative algebraic higher-order theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel , volume 228 of ...

    2022

  21. [29]

    Skew-monoidal reflection and lifting theorems

    Stephen Lack and Ross Street. Skew-monoidal reflection and lifting theorems. Theory and Applications of Categories , 30(28):985--1000, 2015

    2015

  22. [30]

    Categories for the Working Mathematician , volume 5 of Graduate Texts in Mathematics

    Saunders MacLane. Categories for the Working Mathematician , volume 5 of Graduate Texts in Mathematics . Springer, New York, 2nd edition, 1997

    1997

  23. [31]

    Categorical Models of Computation: Partially Traced Categories and Presheaf Models of Quantum Computation

    Octavio Malherbe. Categorical Models of Computation: Partially Traced Categories and Presheaf Models of Quantum Computation . PhD thesis, University of Ottawa, 2010. Available as arXiv:1301.5087

    2010 arXiv

  24. [32]

    Relating categorical semantics for intuitionistic linear logic

    Maria Emilia Maietti, Paola Maneggia, Valeria de Paiva, and Eike Ritter. Relating categorical semantics for intuitionistic linear logic. Applied Categorical Structures , 13(1):1--36, 2005

    2005

  25. [33]

    Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 201...

    2016

  26. [34]

    Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017 , pages 1--12. IEEE Computer Society, 2017

    2017

  27. [35]

    Universal quantitative algebra for fuzzy relations and generalised metric spaces

    Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Universal quantitative algebra for fuzzy relations and generalised metric spaces. Log. Methods Comput. Sci. , 20(4), 2024

    2024

  28. [36]

    Labelled Markov Processes

    Prakash Panangaden. Labelled Markov Processes . Imperial College Press, London, 2009

    2009

  29. [37]

    Quantales

    Jan Paseka and Ji r \' Rosick \`y . Quantales. In Bob Coecke, David Moore, and Alexander Wilce, editors, Current Research in Operational Quantum Logic: Algebras, Categories and Languages , volume 111 of Fundamental Theories of Physics , pages 245--262. Springer, 2000

    2000

  30. [38]

    Towards a semantics for higher-order quantum computation

    Peter Selinger. Towards a semantics for higher-order quantum computation. In Peter Selinger, editor, Proceedings of the Second International Workshop on Quantum Programming Languages (QPL 2004) , volume 33 of TUCS General Publication , pages 127--143, Turku, Finland, 2004. Tur...

    2004

  31. [39]

    Dagger compact closed categories and completely positive maps

    Peter Selinger. Dagger compact closed categories and completely positive maps. Electronic Notes in Theoretical computer science , 170:139--163, 2007

    2007

  32. [40]

    Idempotents in dagger categories

    Peter Selinger. Idempotents in dagger categories. Electronic Notes in Theoretical Computer Science , 210:107--122, 2008

    2008

  33. [41]

    A practical type theory for symmetric monoidal categories

    Michael Shulman. A practical type theory for symmetric monoidal categories. Theory and Applications of Categories , 37(25):863--907, 2021

    2021

  34. [42]

    An introduction to quantaloid-enriched categories

    Isar Stubbe. An introduction to quantaloid-enriched categories. Fuzzy Sets and Systems , 256:95--116, 2014

    2014

  35. [43]

    The Theory of Quantum Information

    John Watrous. The Theory of Quantum Information . Cambridge University Press, Cambridge, 2018

    2018

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.