Pith. sign in

REVIEW 4 major objections 5 minor 43 references

A Rewriting Theory for Quantum Lambda-Calculus

T0 review · 4 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read This paper establishes a rewriting theory for an untyped quantum lambda-calculus with unrestricted β-reduction and measurement: general reduction is confluent, every reduction sequence factorizes as surface steps followed by non-surface…

desk verdict Genuinely new standardization and normalization results for quantum lambda calculus with measurement, but the main theorems rest on a commutation lemma whose proof is missing from the appendix. read the letter →

arxiv 2411.14856 v2 pith:WKG2WHYK submitted 2024-11-22 cs.LO

Claudia Faggian , Gaetan Lopez , Benoît Valiron This is my paper · ORCID
classification cs.LO MSC 03B4068Q4268Q12
keywords quantumlambda-calculusprobabilisticrewritingstandardizationnormalizationconfluencesurfacereductionlinearlogicoperationalsemantics
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

Quantum lambda-calculi have mostly been studied through a fixed call-by-value evaluation strategy, leaving the underlying general rewrite theory largely unexplored. This paper builds an untyped quantum lambda-calculus, Q, on top of Simpson's linear-logic-inspired Λ! calculus, with full β-reduction unrestricted and quantum operations confined to surface contexts. Its central claim is that this system has a genuine rewriting theory: reduction is confluent, any reduction sequence can be reorganized into surface steps followed by non-surface steps (standardization), and surface reduction is a normalizing strategy even when termination is only asymptotic. The motivation is to give quantum programming the same tools that classical λ-calculus has—program transformations, compiler optimizations, parallel schedules, and a robust notion of program equivalence—rather than only a deterministic interpreter.

What carries the argument

The load-bearing object is the probabilistic rewrite system (MD(P), ⇒), where programs are pairs of a quantum memory and a valid term, and rewriting acts on finite multisets of weighted programs called multidistributions. Surface reduction, the paper's evaluation strategy, is the restriction of β-steps to surface contexts plus all quantum steps; surface contexts are contexts whose hole is not under a ! and not inside a branch of meas. The key technical lemmas are a pointed diamond lemma for surface reduction (joining any two surface steps up to register re-indexing), a shape-preservation lemma for non-surface steps, and a modular factorization lemma that organizes any reduction sequence into surface steps followed by non-surface steps.

What would settle it

Check Proposition 4.2 directly. Take the valid program $[\![\,(\frac{|0\rangle+|1\rangle}{\sqrt{2}}\otimes|\varphi\rangle)\,;\, (\lambda x.\,\mathrm{meas}(r_0,x,I))\,r_1\,]\!]$ and fire the surface quantum step that measures $r_0$ inside the linear abstraction. The outcome-$1$ reduct is $[\![\,|\varphi\rangle\,;\,(\lambda x.I)\,r_1\,]\!]$, whose subterm $\lambda x.I$ violates the validity condition that every linear abstraction use its variable exactly once at surface position. A permitted step that produces an invalid term would refute Proposition 4.2 and with it the well-definedness of the system.

Watch

Extended reading notes

Core claim

The paper's core claim is that Q, a probabilistic rewrite system on programs pairing a quantum memory with a valid term, supports the full power of β-reduction while remaining quantum-safe, and that its evaluation strategy is well-behaved. Concretely, Theorem 6.4 establishes confluence of the general reduction; Theorem 6.7 gives surface standardization, stating that any reduction sequence m⇒∗ n can be factored as m⇒s∗ · ⇒¬s∗ n; and Theorem 7.5 gives asymptotic normalization, stating that for every program p the set of limits of general reduction has a greatest element JpK, and that strict surface reduction converges to JpK with probability 1 if any reduction order can do so. These results are meant to provide quantum functional programming with a standardization theorem in the same spirit as Plotkin's call-by-value calculus, but with measurement and probabilistic branching present.

Load-bearing premise

Everything hinges on Proposition 4.2's claim that every reduction step applied to a valid program yields valid programs, including quantum steps fired inside a linear abstraction body; if validity can be lost, the rewrite system is not well-defined on the program set.

Editorial extensions

If this is right

  • Because general reduction is confluent, any two complete computations of the same program that end in surface normal form end in the same program up to register renaming, giving a robust notion of program identity.
  • Standardization means a quantum program can be debugged and optimized at the level of unrestricted β-reduction while trusting that a surface scheduler will reproduce the same outcomes.
  • For programs that only terminate asymptotically, strict surface reduction still finds the highest probability of reaching a surface normal form that any reduction order can achieve.
  • Non-surface steps never change the quantum memory or the shape of a term, so rewriting inside !-boxes is neutral for convergence probability.

Reading between the lines

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

  • Editorial: a typed version of this calculus, along the lines of Selinger and Valiron's quantum lambda calculus, should inherit the same standardization and normalization theorems through the call-by-push-value reading of the Bang operator.
  • Editorial: the asymptotic normalization theorem gives a concrete scheduler for quantum functional programs: at every step reduce every surface redex in every branch, and convergence to the optimal probability is guaranteed by random descent.
  • Editorial: the factorization result suggests that compiler rewrites inside thunked !-boxes are safe program transformations, since postponing non-surface steps does not change the limit of convergence.
  • Editorial: the same combination of multidistribution lifting and surface contexts could be carried over to other affine or resource-sensitive probabilistic calculi, such as linear probabilistic λ-calculi, provided a validity or typing invariant is maintained.
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

4 major / 5 minor

Summary. The paper develops a rewriting theory for an untyped quantum lambda calculus built on Simpson's lambda-calculus. It defines raw terms, validity constraints (linear abstractions, register linearity and surface occurrence), and programs as re-indexing equivalence classes over a quantum memory. Reduction is defined on multidistributions of programs, combining unrestricted beta reduction with surface-only quantum rules (new, unitary gates, measurement). The main results are confluence of the general reduction, a diamond property and random descent for surface reduction, a surface standardization theorem, and an asymptotic normalization theorem stating that strict surface reduction converges to the greatest possible limit of the general reduction. Proofs are distributed between the main text and appendices.

Significance. If the stated results are correct, the paper fills a genuine gap: existing quantum lambda calculi mostly fix a deterministic evaluation strategy, and no standardization result covering measurement and probabilistic behavior has been available. The design of validity constraints and the restriction of quantum rules to surface contexts is natural and well motivated, and the use of monadic probabilistic rewriting is appropriate. The paper also gives a concrete leading example (the fair-coin loop) and a plausible path from factorization to asymptotic normalization. The main weakness is not the conceptual framework but the incompleteness of several load-bearing proofs, in particular Proposition 4.2 and Lemma 6.6, which leaves the central claims unsupported as written. I do not see a circularity problem: the cited prior results are external theorems, and the novelty lies in the quantum-specific argument.

major comments (4)
  1. [§4.1, Proposition 4.2] Proposition 4.2 is asserted without any proof, and it is load-bearing because the reduction relations are defined only on programs, i.e., valid terms with a matching quantum memory. The concrete counterexample (λx.meas(r0,x,I)) r1 does not refute the proposition: that term is not valid under Definition 3.2, because the unique occurrence of x in λx.meas(r0,x,I) lies in the second branch of meas, which is not a surface context. The proposition may well be true, but the absence of a proof of validity preservation remains a gap that should be filled.
  2. [Appendix D, Lemma 6.6] Lemma 6.6 is the second hypothesis of the modular factorization Lemma 6.5 and therefore underpins Theorem 6.7 (surface standardization), and via Lemma E.1 also Theorems 7.4 and 7.5. The main text says 'The proof is in the Appendix,' but Appendix D merely repeats the lemma statement and the same one-line induction sketch, with no case analysis for the shape-preservation argument or for the possible shapes of the surface context S. As written, the standardization theorem is unsupported and the asymptotic normalization result inherits the gap.
  3. [Appendix D, Lemma D.2] Lemma D.2 (redex and normal-form preservation under non-surface beta steps) is used in the proof of Theorem 7.4 via Lemma E.1, but it is only stated as 'an easy-to-verify consequence' of shape preservation and no proof is supplied. It is a plausible statement, but since it is needed for the normalization result, it should be proved or at least derived in detail.
  4. [Appendix C, Lemma 6.2] The proof of the pointed diamond is a high-level case analysis that leaves several verification steps implicit. In particular, in the meas/meas case the equality m11 + m12 = m21 + m22 is asserted without exhibiting the probability arithmetic, and the overlapping-redex treatment relies on unstated context-disjointness assumptions. Since Proposition 6.3 and Theorem 7.3 depend on this lemma, the proof should be expanded to make those steps checkable.
minor comments (5)
  1. [Appendix C, case 2b] The notation 'Ui AQ);' contains an unmatched parenthesis and should be written as U^i_A(Q).
  2. [Appendix C, case 2f] The expression 'πj 0circπi 1' is missing the composition symbol and should read π^j_0 ∘ π^i_1.
  3. [Theorem 7.5] Item (1.) says 'the limit Lim(p,⇒) has a greatest element', but Lim(p,⇒) is a set by Definition 7.2; it should say 'the set Lim(p,⇒) has a greatest element'.
  4. [Definition 3.2] The phrase 'every occurrences of registers are surface' is ungrammatical; it should be 'every occurrence of a register is surface'. The definition of an occurrence is only given informally before the definition, so a small clarification of the notion of surface occurrence of a register would help.
  5. [References] Reference [25] is the arXiv version of the present paper; if this is an extended journal version, the reference should be updated to the published CSL 2025 version and the relationship between the two versions should be stated.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: self-cited lemmas are external and parameter-free; the real weakness is an unproved standardization lemma, not a circular reduction.

full rationale

The derivation chain is not circular. The central theorems are obtained by combining (i) the pointed diamond Lemma 6.2, proved by induction in Appendix C; (ii) Simpson's surface standardization for the pure Lambda! calculus [43]; (iii) the modular factorization Lemma 6.5 from [1]; and (iv) the asymptotic-completeness criterion Lemma E.1 from [24]. Although [1] and [24] are self-citations (they share author Faggian), they are external, published, parameter-free theorems about abstract or linear-logic rewriting whose statements do not include the quantum target results; hence under the review rules they count as independent evidence, not as circular input. No equation of the paper defines a target quantity in terms of itself, and no fitted value is renamed as a prediction. Flagged non-circular gaps: Proposition 4.2 ('Validity. Validity of terms is preserved') is stated without proof in Section 4.1; Lemma 6.6, which is condition 2 of the modular factorization and therefore load-bearing for Theorems 6.7 and 7.5, is only sketched in Appendix D ('We exploit in an essential way the fact that M and P have the same shape') with no induction or case analysis; and Theorem 7.3 is asserted as a consequence of Lemma 6.2 without a detailed proof. These are completeness and correctness risks, not circularity: the missing arguments, if supplied, would reduce to the paper's own definitions and cases. The reader's proposed counterexample to Proposition 4.2 does not land: (lambda x.meas(r0,x,I)) r1 is not valid under Definition 3.2, because the required unique surface occurrence of x would be inside a meas branch, and branch positions are not surface contexts. Score 2 reflects the presence of several self-citations in the proof infrastructure but no load-bearing reduction of a claim to its own input.

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

No free parameters. The central claim rests on external rewriting-theory results (Simpson's standardization; the asymptotic completeness criterion of [24]; the pointwise criterion of [26]) and on the paper's own assumption that its validity conditions are preserved by reduction. The latter is false, as detailed in red flags. No invented entities are introduced.

assumptions (4)
  • standard math Simpson's surface standardization for the pure Λ! calculus (Simpson 2005)
    Used as condition 1 in Lemma 6.5 to prove surface standardization (Theorem 6.7). The quantum calculus inherits this factorization of β-reduction for the underlying Λ! calculus.
  • standard math Asymptotic completeness criterion of Faggian and Guerrieri (2021)
    Reformulated as Lemma E.1 and used to prove Theorem 7.4; the paper does not prove this criterion or fully verify its hypotheses in the quotient-by-reindexing setting.
  • domain assumption Validity constraints of Definition 3.2 are preserved by all reduction rules (Proposition 4.2)
    This is the load-bearing closure assumption. It is false: see counterexample in red flags. Without it, reduction can leave the set of programs.
  • standard math Pointwise criterion of Faggian and Ronchi Della Rocca (2019)
    Used in Appendix C to lift the pointed diamond property to the diamond property for surface reduction.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Rewriting Theory for Quantum Lambda-Calculus." pith.science (2026). https://pith.science/paper/WKG2WHYK

@misc{pith2026241114856,
  author       = {Pith},
  title        = {Pith review of: A Rewriting Theory for Quantum Lambda-Calculus},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WKG2WHYK}},
  note         = {Machine review of arXiv:2411.14856}
}
read the original abstract

Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.

Figures

Figures reproduced from arXiv: 2411.14856 by the authors.

Figure 2
Figure 2. π0 the 0-projection on a state Q, π0(Q) := Q0 π1 the 1-projection on a state Q, π1(Q) := Q1 σi the permutation that swaps i to 0, σi(i) := 0, σi(0) := i and σi(k) := k otherwise µi the permutation that swaps i to the last integer position of a register in a state, for example if Q has n+1 qubits, µi(i) = n σi,j the permutation that swaps i to 0, j to 1, σi,j (i) := 0, σi,j (0) := i, σi,j (j) := 1, σi,j (1) := j and … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 26 canonical work pages

  1. [1]

    Factorize factorization

    Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize factorization. In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference) , volume 183 of LIPIcs , pages 6:1--6:25. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2021. https://doi.org/10.4230/LIPIcs.CSL.20...

    work page doi:10.4230/lipics.csl.2021.6 2021

  2. [2]

    Ariola and Stefan Blom

    Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic , 117(1):95 -- 168, 2002

    work page 2002

  3. [3]

    The benefits of diligence

    Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. International Joint Conference on Automated Reasoning, IJCAR 2024, , 2024

    work page 2024

  4. [4]

    The vectorial lambda-calculus

    Pablo Arrighi, Alejandro D \' az-Caro, and Beno \^ t Valiron. The vectorial lambda-calculus. Information and Computation , 254:105--139, 2017. https://doi.org/10.1016/j.ic.2017.04.001 doi:10.1016/j.ic.2017.04.001

    doi:10.1016/j.ic.2017.04.001 2017

  5. [5]

    Lineal: A linear-algebraic lambda-calculus

    Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Logical Methods in Computer Science , 13(1), 2017

    work page 2017

  6. [6]

    On probabilistic term rewriting

    Martin Avanzini, Ugo Dal Lago , and Akihisa Yamada. On probabilistic term rewriting. Sci. Comput. Program. , 185, 2020. URL: https://doi.org/10.1016/j.scico.2019.102338, https://doi.org/10.1016/J.SCICO.2019.102338 doi:10.1016/J.SCICO.2019.102338

    work page arXiv 2020

  7. [7]

    The Lambda Calculus -- Its Syntax and Semantics , volume 103 of Studies in logic and the foundations of mathematics

    Hendrik Pieter Barendregt. The Lambda Calculus -- Its Syntax and Semantics , volume 103 of Studies in logic and the foundations of mathematics . North-Holland, 1984

    work page 1984

  8. [8]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '20 , pages 286--300. ACM , 2020...

    arXiv 2020

Show all 43 references
  1. [9]

    Proving positive almost sure termination under strategies

    Olivier Bournez and Florent Garnier. Proving positive almost sure termination under strategies. In Rewriting Techniques and Applications, RTA , pages 357--371, 2006

    2006

  2. [10]

    The bang calculus revisited

    Antonio Bucciarelli, Delia Kesner, Alejandro R \' os, and Andr \' e s Viso. The bang calculus revisited. Inf. Comput. , 293:105047, 2023. URL: https://doi.org/10.1016/j.ic.2023.105047, https://doi.org/10.1016/J.IC.2023.105047 doi:10.1016/J.IC.2023.105047

    2023

  3. [11]

    An automated deductive verification framework for circuit-building quantum programs

    Christophe Chareton, S \' e bastien Bardin, Fran c ois Bobot, Valentin Perrelle, and Beno \^ t Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, Proceedings of the 30th European Symposium on Programming Lan...

    2021 doi

  4. [12]

    The geometry of parallelism: classical, probabilistic, and quantum effects

    Ugo Dal Lago , Claudia Faggian, Beno \^ t Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming La...

    2017 doi

  5. [13]

    On a measurement-free quantum lambda calculus with classical control

    Ugo Dal Lago , Andrea Masini, and Margherita Zorzi. On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci. , 19(2):297--335, 2009. https://doi.org/10.1017/S096012950800741X doi:10.1017/S096012950800741X

    2009 doi

  6. [14]

    Confluence results for a quantum lambda calculus with measurements

    Ugo Dal Lago , Andrea Masini, and Margherita Zorzi. Confluence results for a quantum lambda calculus with measurements. Electr. Notes Theor. Comput. Sci. , 270(2):251--261, 2011. https://doi.org/10.1016/j.entcs.2011.01.035 doi:10.1016/j.entcs.2011.01.035

    2011 doi

  7. [15]

    Probabilistic operational semantics for the lambda calculus

    Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl. , 46(3):413--450, 2012. https://doi.org/10.1051/ita/2012012 doi:10.1051/ita/2012012

    2012

  8. [16]

    Non deterministic extensions of untyped lambda-calculus

    Ugo de'Liguoro and Adolfo Piperno. Non deterministic extensions of untyped lambda-calculus. Inf. Comput. , 122(2):149--177, 1995

    1995

  9. [17]

    Probabilistic lambda-calculus and quantitative program analysis

    Alessandra Di Pierro , Chris Hankin, and Herbert Wiklicky. Probabilistic lambda-calculus and quantitative program analysis. J. Log. Comput. , 15(2):159--179, 2005

    2005

  10. [18]

    Realizability in the unitary sphere

    Alejandro D \' az - Caro, Mauricio Guillermo, Alexandre Miquel, and Beno \^ t Valiron. Realizability in the unitary sphere. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19 , pages 1--13. IEEE , 2019. https://doi.org/10.1109/LICS.2019...

    2019

  11. [19]

    Confluence in probabilistic rewriting

    Alejandro D \' az - Caro and Guido Martinez. Confluence in probabilistic rewriting. Electr. Notes Theor. Comput. Sci. , 338:115--131, 2018

    2018

  12. [20]

    The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value

    Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016) , pages 174--187. ACM, 2016. htt...

    2016

  13. [21]

    The computational meaning of probabilistic coherence spaces

    Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada , pages 87--96. IEEE Computer...

    2011 doi

  14. [22]

    Probabilistic rewriting: Normalization, termination, and unique normal forms

    Claudia Faggian. Probabilistic rewriting: Normalization, termination, and unique normal forms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany , volume 131 of LIPIcs , pa...

    2019 doi

  15. [23]

    Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms

    Claudia Faggian. Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms. Log. Methods Comput. Sci. , 18(2), 2022. URL: https://doi.org/10.46298/lmcs-18(2:5)2022, https://doi.org/10.46298/LMCS-18(2:5)2022 doi:10.46298/LMCS-18(2:5)2022

    2022 doi

  16. [24]

    Factorization in call-by-name and call-by-value calculi via linear logic

    Claudia Faggian and Giulio Guerrieri. Factorization in call-by-name and call-by-value calculi via linear logic. In Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 , volume 12650 of Lecture Notes in Computer Science , pag...

    2021 doi

  17. [25]

    A rewriting theory for quantum -calculus

    Claudia Faggian, Gaetan Lopez, and Beno\^it Valiron. A rewriting theory for quantum -calculus. CoRR , abs/2411.14856, 2024. URL: http://arxiv.org/abs/2411.14856

    2024 arXiv

  18. [26]

    Lambda calculus and probabilistic computation

    Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019 , pages 1--13. IEEE , 2019. https://doi.org/10.1109/LICS.2019.878569...

    2019

  19. [27]

    A relational theory of monadic rewriting systems, part I

    Francesco Gavazzo and Claudia Faggian. A relational theory of monadic rewriting systems, part I . In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 , pages 1--14. IEEE , 2021. https://doi.org/10.1109/LICS52264.2021.9...

    2021

  20. [28]

    Simon J. Gay. Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science , 16(4):581--600, 2006. https://doi.org/10.1017/S0960129506005378 doi:10.1017/S0960129506005378

    2006 doi

  21. [29]

    Linear logic

    Jean - Yves Girard. Linear logic. Theor. Comput. Sci. , 50:1--102, 1987. https://doi.org/10.1016/0304-3975(87)90045-4 doi:10.1016/0304-3975(87)90045-4

    1987 doi

  22. [30]

    Green, Peter LeFanu Lumsdaine, Neil J

    Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Beno \^ t Valiron. Quipper: A scalable quantum programming language. In Hans-Juergen Boehm and Cormac Flanagan, editors, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and I...

    2013

  23. [31]

    The bang calculus and the two G irard's translations

    Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two G irard's translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018) , volume 292 of EPTCS , pages 15--30, 2019. https://doi.org/10...

    2018 doi

  24. [32]

    From innermost to full almost-sure termination of probabilistic term rewriting

    Jan - Christoph Kassing, Florian Frohn, and J \" u rgen Giesl. From innermost to full almost-sure termination of probabilistic term rewriting. In Naoki Kobayashi and James Worrell, editors, Foundations of Software Science and Computation Structures - 27th International Confere...

    2024

  25. [33]

    Kirkeby and Henning Christiansen

    Maja H. Kirkeby and Henning Christiansen. Confluence and convergence in probabilistically terminating reduction systems. In Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017 , pages 164--179, 2017

    2017

  26. [34]

    Emanuel H. Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory, Los Alamos, New Mexico, US., 1996

    1996

  27. [35]

    Concrete categorical model of a quantum circuit description language with measurement

    Dongho Lee, Valentin Perrelle, Beno \^ t Valiron, and Zhaowei Xu. Concrete categorical model of a quantum circuit description language with measurement. In Mikolaj Bojanczyk and Chandra Chekuri, editors, Proceedings of the 41st IARCS Annual Conference on Foundations of Softwar...

    2021 doi

  28. [36]

    M.H.A. Newman. On theories with a combinatorial definition of equivalence. Annals of Mathematics , 43(2), 1942

    1942

  29. [37]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information . Cambridge University Press, 2002

    2002

  30. [38]

    Applying quantitative semantics to higher-order quantum computing

    Michele Pagani, Peter Selinger, and Beno \^ t Valiron. Applying quantitative semantics to higher-order quantum computing. In Suresh Jagannathan and Peter Sewell, editors, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( POPL'14 ) , ...

    2014

  31. [39]

    qPCF: higher-order languages and quantum circuits

    Luca Paolini, Mauro Piccolo, and Margherita Zorzi. qPCF: higher-order languages and quantum circuits. Journal of Automated Reasoning , 63(4):941--966, 2019. https://doi.org/10.1007/s10817-019-09518-y doi:10.1007/s10817-019-09518-y

    2019 doi

  32. [40]

    QWIRE: a core language for quantum circuits

    Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17 , pages 846--858. ACM , 2017. http...

    2017

  33. [41]

    Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. , 1(2):125--159, 1975

    1975

  34. [42]

    A lambda calculus for quantum computation with classical control

    Peter Selinger and Beno \^i t Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science , 16:527--552, 2006. https://doi.org/10.1017/S0960129506005238 doi:10.1017/S0960129506005238

    2006 doi

  35. [43]

    Alex K. Simpson. Reduction in a linear lambda-calculus with applications to operational semantics. In Term Rewriting and Applications, 16th International Conference ( RTA 2005) , volume 3467 of Lecture Notes in Computer Science , pages 219--234, 2005. https://doi.org/10.1007/9...

    2005 doi

Pith tools

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