Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability

Giorgio Bacci; Rasmus Ejlers M{\o}gelberg

arxiv: 2501.18275 · v3 · pith:IIBSCLHVnew · submitted 2025-01-30 · 💻 cs.LO · math.LO

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability

Giorgio Bacci , Rasmus Ejlers M{\o}gelberg This is my paper

Pith reviewed 2026-05-23 04:44 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords quantitative logicguarded recursionprobability measuresinduction principlesKantorovich distanceMarkov processesaffine calculusbisimilarity distances

0 comments

The pith

An affine calculus and higher-order quantitative logic equip probability measures with guarded recursion and induction principles.

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

The paper builds a quantitative logic for reasoning about the degree to which properties hold in probabilistic programs and processes. It starts with an affine calculus over 1-bounded complete metric spaces and the probability monad under the Kantorovich distance, interpreting guarded recursion through Banach fixed points. The logic then adds novel principles for guarded recursion together with induction rules for probability measures and natural numbers. These tools are applied to bound bisimilarity distances between Markov processes and to prove convergence of a temporal learning algorithm and a random walk via coupling. A reader cares because the principles supply concrete reasoning steps for verifying recursive probabilistic behavior with quantitative guarantees.

Core claim

The authors construct an affine calculus for 1-bounded complete metric spaces and the monad of probability measures equipped with the Kantorovich distance. Guarded recursion in the calculus is interpreted via Banach's fixed point theorem. They then define an affine higher-order quantitative logic for terms of this calculus that includes novel principles for guarded recursion and induction over probability measures and natural numbers, illustrated by proofs of upper bounds on bisimilarity distances, convergence of a temporal learning algorithm, and convergence of a random walk.

What carries the argument

The affine higher-order quantitative logic containing guarded recursion principles interpreted via Banach fixed points together with induction principles over probability measures and natural numbers.

If this is right

Upper bounds on bisimilarity distances between Markov processes become provable inside the logic.
Convergence of a temporal learning algorithm follows from a coupling argument formalised in the logic.
Convergence of a random walk follows from a coupling argument formalised in the logic.
Recursive probabilistic programs and processes can be verified using the guarded recursion principle.

Where Pith is reading between the lines

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

The same induction principles could be instantiated for other distances or monads that satisfy the required metric completeness conditions.
The logic might serve as a target for embedding existing quantitative type systems or probabilistic program logics.
Case studies could be extended to verify convergence rates rather than mere convergence in iterative probabilistic algorithms.

Load-bearing premise

The guarded recursion is soundly interpreted via Banach's fixed point theorem on the 1-bounded complete metric spaces and the probability monad with Kantorovich distance.

What would settle it

A concrete recursive probabilistic process or Markov chain for which the logic's induction or guarded recursion principle derives an incorrect bound on the Kantorovich distance between behaviors.

Figures

Figures reproduced from arXiv: 2501.18275 by Giorgio Bacci, Rasmus Ejlers M{\o}gelberg.

**Figure 1.** Figure 1: Typing rules. Example 5.1 (The geometric distribution). The geometric distribution geo𝑝 : D (N) should satisfy geo𝑝 ≡ 𝛿 (0) ⊕𝑝 D (succ) (geo𝑝 ). To type check this as a fixed point, first note that the functorial action of D can be defined as D (𝑓 ) ≜ 𝜆𝑥.let 𝑎 = 𝑥 in 𝑓 (𝑎) : D (𝐴) ⊸𝑟 D (𝐵) when 𝑓 : 𝐴 ⊸𝑟 𝐵 for 𝑟 < ∞. In particular, D (succ) : D (N) ⊸1 D (N). So geo𝑝 can be defined as geo𝑝 ≜ fix 𝑥.𝛿 (0) ⊕𝑝 D… view at source ↗

**Figure 2.** Figure 2: Judgemental equality. To these should be added the axioms of IB algebras of Definition [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗

**Figure 3.** Figure 3: Typing rules for logical predicates. JttK ≜ 0 JffK ≜ 1 J𝑡 =𝐴 𝑢K ≜ 𝑑J𝐴K ◦ (J𝑡K ⊗ J𝑠K) ◦ split J𝜑 •𝜓K ≜ ⊕ ◦ (J𝜑K ⊗ J𝜓K) ◦ split J𝜑 −•𝜓K ≜ ⊸ ◦ (J𝜑K ⊗ J𝜓K) ◦ split J𝑟𝜑K ≜ min{𝑟 · −, 1} ◦ 𝑟 J𝜑K ◦ dist J¬𝜑K ≜ 1 − J𝜑K J𝜑 ∧𝜓K ≜ max ◦⟨J𝜑K, J𝜓K⟩ J𝜑 ∨𝜓K ≜ min ◦⟨J𝜑K, J𝜓K⟩ J∃𝑥 : 𝐴.𝜑K ≜ inf ◦ curry(J𝜑K) J∀𝑥 : 𝐴.𝜑K ≜ sup ◦ curry(J𝜑K) [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗

**Figure 4.** Figure 4: Interpretation of logical predicates. Lemma 6.1. The following are all non-expansive maps (where 𝑟 > 0) ⊕, ⊸: Prop ⊗ Prop → Prop min{𝑟 · −, 1} : 𝑟Prop → Prop sup, inf : (∞𝑋 ⊸ Prop) → Prop max, min: Prop × Prop → Prop 𝑑𝑋 : 𝑋 ⊗ 𝑋 → Prop A predicate in context Γ is a term 𝜙 such that Γ ⊢ 𝜙 : Prop. Observe that predicates can be constructed not just using the constructions of [PITH_FULL_IMAGE:figures/full_fig… view at source ↗

**Figure 5.** Figure 5: Logic. (The logical judgments appearing above are assumed to be well-formed) [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗

**Figure 6.** Figure 6: The commands rf and ri. and so combining this with 𝛿 (𝑠[𝑙 ↦→ 1], 𝑠′ ) ∈ Cpltt (𝑠[𝑙 ↦→ 1], JskipK𝑠 ′ ) by Lemma 7.5 we get a coupling between J𝑐 ′ K𝑠 ⊕1 2 𝛿 (𝑠[𝑙 ↦→ 1]) and JskipK𝑠 ′ = 𝛿 (𝑠 ′ ). 11.3 Example: PRP/PRF Switching Lemma In this example, we compute an upper bound on the distance between a random permutation and a random function. This result is part of the classical PRP/PRF switching lemma [12, … view at source ↗

**Figure 7.** Figure 7: Set-theoretic denotation of terms. We denote by [PITH_FULL_IMAGE:figures/full_fig_p037_7.png] view at source ↗

read the original abstract

Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for $1$-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion, and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper builds a quantitative logic with new guarded recursion and induction rules over probability measures, using standard metric semantics.

read the letter

The core contribution is an affine calculus over 1-bounded complete metric spaces with the Kantorovich probability monad, plus a higher-order quantitative logic that adds guarded recursion (via Banach fixed point) and induction principles for probability measures and natural numbers. The case studies then apply this to bound bisimilarity distances on Markov processes and to show convergence for a temporal learning algorithm and a random walk via couplings. That setup is what a reader should expect to see developed in the full text. The approach lines up with existing metric semantics for probabilistic computation, and the choice to keep the calculus affine avoids some of the usual complications with higher-order quantitative reasoning. The case studies are concrete enough to illustrate the intended use for distance and convergence arguments that standard logics handle less directly. The main limitation at this stage is that the abstract alone does not display the actual syntax of the induction rules or the soundness arguments, so it is not yet possible to judge how much the new principles differ from prior quantitative logics in the literature or whether the proofs go through without additional assumptions. The construction itself does not appear to introduce circularity or free parameters. This work is aimed at researchers already working on quantitative program logics and probabilistic process algebra. A specialist in that niche would get value from the explicit rules and the worked examples, even if the broader impact depends on how cleanly the soundness is established. I would send it to peer review so that the derivations and case studies can be checked in detail.

Referee Report

0 major / 2 minor

Summary. The paper constructs an affine calculus for 1-bounded complete metric spaces and the monad of probability measures equipped with the Kantorovich distance. Guarded recursion is included and interpreted via Banach's fixed point theorem. An affine higher-order quantitative logic is then defined over this calculus, featuring novel principles for guarded recursion together with induction over probability measures and natural numbers. Expressivity is demonstrated through case studies on upper bounds for bisimilarity distances of Markov processes, convergence of a temporal learning algorithm, and convergence of a random walk via coupling.

Significance. If the soundness claims hold, the work supplies a higher-order quantitative logic with tailored induction and recursion principles for probabilistic systems. This extends metric semantics techniques (Kantorovich distance, Banach fixed point) into an affine setting with explicit induction rules, offering a potential foundation for verifying properties of recursive probabilistic programs and processes. The case studies provide concrete illustrations of applicability to bisimilarity and convergence arguments.

minor comments (2)

[Abstract / Introduction] The abstract states that the logic includes 'novel principles for guarded recursion, and induction over probability measures and natural numbers,' but does not indicate whether these principles are derived from the calculus or introduced as axioms; a brief clarification in the introduction or §3 would help readers assess novelty.
[Case studies section] The case-study descriptions (bisimilarity distances, temporal learning convergence, random-walk coupling) are summarized at a high level; adding one or two key equations or distance bounds from each study would strengthen the claim of expressivity without lengthening the paper substantially.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, assessment of significance, and recommendation for minor revision. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation constructs an affine calculus over 1-bounded complete metric spaces with the Kantorovich probability monad, interprets guarded recursion via the external Banach fixed-point theorem, and defines a quantitative logic with induction principles. These steps rely on standard metric semantics and fixed-point theorems rather than reducing any claimed result to fitted parameters, self-definitions, or load-bearing self-citations. The case studies apply the logic to bisimilarity distances and convergence arguments without internal circular reductions. The central claims remain independent of the paper's own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based solely on the abstract, the paper relies on standard mathematical background rather than new free parameters or invented entities; the central constructions appear to rest on the affinity assumption and Banach fixed-point interpretation.

axioms (1)

standard math Banach's fixed point theorem applies to interpret guarded recursion on the 1-bounded complete metric spaces and probability monad
Invoked in the abstract to give semantics to the guarded recursion in the calculus.

pith-pipeline@v0.9.0 · 5679 in / 1217 out tokens · 32352 ms · 2026-05-23T04:44:19.183617+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean (Jcost, washburn_uniqueness_aczel); Foundation/DimensionForcing.lean (8-tick, D=3) reality_from_one_distinction; J_uniquely_calibrated_via_higher_derivative unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We construct an affine calculus for 1-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem... induction over probability measures and natural numbers.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Quantitative Linear Logic
cs.LO 2026-05 unverdicted novelty 8.0

pQLL calculi make proof validity and sequent provability real-valued quantities, generalizing hypersequent calculi and deep inference while proving cut-elimination and completeness for soft residuated lattices.
Quantitative Linear Logic
cs.LO 2026-05 accept novelty 8.0

pQLL calculi assign real-valued strength to proofs, generalize hypersequent and deep inference systems, prove cut elimination, and achieve completeness for soft residuated lattices, recovering MALL as p goes to infinity.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages · cited by 1 Pith paper

[1]

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ...

work page doi:10.1007/978-3-319-89884-1_8 2018
[2]

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja

work page
[3]

A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5, POPL (2021), 1–28. https://doi.org/10.1145/3434333

work page doi:10.1145/3434333 2021
[4]

Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. 2024. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8, ICFP (2024), 284–316. https://doi.org/10.1145/3674635

work page doi:10.1145/3674635 2024
[5]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, and Pierre-Yves Strub. 2023. Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. (2023), 215. https://eprint.iacr.org/ 2023/215

work page 2023
[6]

Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic. Proc. ACM Program. Lang. 9, POPL (2025), 1167–1195. https://doi.org/10.1145/3704876

work page doi:10.1145/3704876 2025
[7]

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni. 2024. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8, OOPSLA1 (2024), 784–809

work page 2024
[8]

Larsen, and Radu Mardare

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. 2018. A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains. Log. Methods Comput. Sci. 14, 4 (2018)

work page 2018
[9]

Kwiatkowska

Christel Baier and Marta Z. Kwiatkowska. 2000. Domain equations for probabilistic processes. Math. Struct. Comput. Sci. 10, 6 (2000), 665–717. http://journals.cambridge.org/action/displayAbstract?aid=71051

work page 2000
[10]

Stefan Banach. 1922. Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales. Fundamenta Mathematicae 3, 1 (1922), 133–181

work page 1922
[11]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy (LIPIcs, Vol. 55), Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi (Eds.). Schloss...

work page doi:10.4230/lipics.icalp.2016.107 2016
[12]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 , Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 90–101. https: //doi.org/10.1145/1...

work page doi:10.1145/1480881.1480894 2009
[13]

Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. IACR Cryptol. ePrint Arch. (2004), 331. http://eprint.iacr.org/2004/331

work page 2004
[14]

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8, 4 (2012). https://doi.org/10. 2168/LMCS-8(4:1)2012

work page 2012
[15]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Note...

work page doi:10.1007/978-3-642- 2014
[16]

Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

work page
[17]

In10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK (LIPIcs, Vol

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK (LIPIcs, Vol. 337) , Maribel Fernández (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2:1–2:20. https: //doi.org/10.423...

work page doi:10.4230/lipics.fscd.2025.2 2025
[18]

Francesco Dagnino and Fabio Pasquali. 2022. Logical Foundations of Quantitative Equality. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , Christel Baier and Dana Fisman (Eds.). ACM, 16:1–16:13. https://doi.org/10.1145/3531130.3533337

work page doi:10.1145/3531130.3533337 2022
[19]

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. 2017. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 545–556. https://doi.org/1...

work page doi:10.1145/3009837.3009890 2017
[20]

de Vink and Jan J

Erik P. de Vink and Jan J. M. M. Rutten. 1999. Bisimulation for Probabilistic Transition Systems: A Coalgebraic Approach. Theor. Comput. Sci. 221, 1-2 (1999), 271–293. https://doi.org/10.1016/S0304-3975(99)00035-3

work page doi:10.1016/s0304-3975(99)00035-3 1999
[21]

Desharnais, V

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. 2000. Approximation of Labeled Markov Processes. In Proceedings of the Fifteenth Annual IEEE Symposium On Logic In Computer Science . IEEE Computer Society Press, 95–106

work page 2000
[22]

Orchard, Flavien Breuvart, and Tarmo Uustalu

Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining effects and coeffects via grading. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 476–489. h...

work page doi:10.1145/2951913.2951939 2016
[23]

Haselwarter, Joseph Tassarotti, and Lars Birkedal

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8, POPL (2024), 753–784. https://doi.org/10.1145/3632868

work page doi:10.1145/3632868 2024
[24]

Wagner, John Kelsey, and Bruce Schneier

Chris Hall, David A. Wagner, John Kelsey, and Bruce Schneier. 1998. Building PRFs from PRPs. In Advances in Cryptology - CRYPTO ’98, 18th Annual International Cryptology Conference, Santa Barbara, California, USA, August 23-27, 1998, Proceedings (Lecture Notes in Computer Science, Vol. 1462) , Hugo Krawczyk (Ed.). Springer, 370–389. https://doi.org/10.100...

work page doi:10.1007/bfb0055742 1998
[25]

Alessandro Giacalone Chi-Chang Jou and Scott A. Smolka. 1994. Algebraic Reasoning for Probabilistic Concurrent Systems. In PROCOMET. North Holland, 443–458

work page 1994
[26]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162–178. https://doi.org/10.1016/0022- 0000(85)90012-1

work page doi:10.1016/0022- 1985
[27]

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. 2022. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , Christel Baier and Dana Fisman (Eds.). ACM, 42:1–42:13. https: //doi.org/...

work page doi:10.1145/3531130.3533359 2022
[28]

Kim Guldstrand Larsen and Arne Skou. 1991. Bisimulation through Probabilistic Testing. Information and Computation 94, 1 (1991), 1–28

work page 1991
[29]

William F. Lawvere. 1973. Metric spaces, generalized logic, and closed categories. In Seminario Mat. e. Fis. di Milano , Vol. 43. Springer, 135–166

work page 1973
[30]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2016. Quantitative Algebraic Reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016 , Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 700–709. https://doi.org/10.1145/2933575.2934518 , Vol. 1, No. 1, A...

work page doi:10.1145/2933575.2934518 2016
[31]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2018. Free complete Wasserstein algebras. Log. Methods Comput. Sci. 14, 3 (2018). https://doi.org/10.23638/LMCS-14(3:19)2018

work page doi:10.23638/lmcs-14(3:19)2018 2018
[32]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2021. Fixed-Points for Quantitative Equational Logics. In LICS. IEEE, 1–13

work page 2021
[33]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems . Springer. https://doi.org/10.1007/B138392

work page doi:10.1007/b138392 2005
[34]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18, 3 (1996), 325–353. https://doi.org/10.1145/229542.229547

work page doi:10.1145/229542.229547 1996
[35]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 672–681. https://doi.o...

work page doi:10.1145/2933575.2935317 2016
[36]

Jason Reed and Benjamin C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 , Paul Hudak and Stephanie Weirich (Eds.). ACM, 157–168. https: //doi.org/10.1145/1863543.1863568

work page doi:10.1145/1863543.1863568 2010
[37]

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . https: //homotopytypetheory.org/book, Institute for Advanced Study

work page 2013
[38]

Franck van Breugel. 2005. A Behavioural Pseudometric for Metric Labelled Transition Systems. In CONCUR (Lecture Notes in Computer Science, Vol. 3653) . Springer, 141–155

work page 2005
[39]

Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. 2005. An Accessible Approach to Behavioural Pseudometrics. In ICALP (Lecture Notes in Computer Science, Vol. 3580) . Springer, 1018–1030

work page 2005
[40]

Franck van Breugel and James Worrell. 2005. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331, 1 (2005), 115–142. , Vol. 1, No. 1, Article . Publication date: July 2025. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability 29 A OMITTED PROOFS OF SECTION 2 We start by reviewing some ...

work page 2005
[41]

Observe that any Δ can always be described as the sum Δ = Δ1 + 𝑟 Δ2, for appropriate Δ1, Δ2. By inductive hypothesis, then the following is derivable: Γ1, Δ1, Γ′ 1 ⊢ 𝑡 : 𝐵 ⊸𝑝 𝐴 Γ2, Δ2, Γ′ 2 ⊢ 𝑢 : 𝐵 (Γ1, Δ1, Γ′ 1 ) + 𝑟 (Γ′ 2, Δ2, Γ′ 2 ) ⊢ 𝑡 𝑢 : 𝐵 (app) and Γ, Δ, Γ′ = (Γ1, Δ1, Γ′ 1 ) + 𝑟 (Γ′ 2, Δ2, Γ′ 2 ). Case (⊗): Assume Γ, Γ′ ⊢ ( 𝑡, 𝑢) : 𝐴 𝑟 ⊗𝑠𝐵 was deri...

work page
[42]

Case (fix): Assume Γ, Γ′ ⊢ fix 𝑥 .𝑡 : 𝐴 was derived with an application of (fix) and that 𝑥 ∉ Δ (otherwise apply 𝛼-renaming to 𝑡)

By inductive hypothesis, then the following is derivable: Γ1, Δ, Γ′ 1 ⊢ 𝑡 : D𝐴 Γ2, Δ, Γ′ 2 ⊢ 𝑢 : D𝐴 𝑝 ∈ ( 0, 1) 𝑝 (Γ1, Δ, Γ′ 1 ) + ( 1 − 𝑝) (Γ2, Δ, Γ′ 2 ) ⊢ 𝑡 ⊕𝑝 𝑢 : D𝐴 (⊕𝑝 ) and Γ, Δ, Γ′ = 𝑝 (Γ1, Δ, Γ′ 1 ) + ( 1 − 𝑝) (Γ2, Δ, Γ′ 2 ). Case (fix): Assume Γ, Γ′ ⊢ fix 𝑥 .𝑡 : 𝐴 was derived with an application of (fix) and that 𝑥 ∉ Δ (otherwise apply 𝛼-renaming...

work page 2025
[43]

Then from the sub-derivations of Γ1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 and Γ′ 1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 occurring above, by Lemma 5.7, we , Vol

Let Γ∞ be the version of Γ where all sensitivities are set to ∞. Then from the sub-derivations of Γ1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 and Γ′ 1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 occurring above, by Lemma 5.7, we , Vol. 1, No. 1, Article . Publication date: July 2025. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability 41 obtain new derivations such that the fol...

work page 2025

[1] [1]

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ...

work page doi:10.1007/978-3-319-89884-1_8 2018

[2] [2]

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja

work page

[3] [3]

A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5, POPL (2021), 1–28. https://doi.org/10.1145/3434333

work page doi:10.1145/3434333 2021

[4] [4]

Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. 2024. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8, ICFP (2024), 284–316. https://doi.org/10.1145/3674635

work page doi:10.1145/3674635 2024

[5] [5]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, and Pierre-Yves Strub. 2023. Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. (2023), 215. https://eprint.iacr.org/ 2023/215

work page 2023

[6] [6]

Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic. Proc. ACM Program. Lang. 9, POPL (2025), 1167–1195. https://doi.org/10.1145/3704876

work page doi:10.1145/3704876 2025

[7] [7]

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni. 2024. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8, OOPSLA1 (2024), 784–809

work page 2024

[8] [8]

Larsen, and Radu Mardare

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. 2018. A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains. Log. Methods Comput. Sci. 14, 4 (2018)

work page 2018

[9] [9]

Kwiatkowska

Christel Baier and Marta Z. Kwiatkowska. 2000. Domain equations for probabilistic processes. Math. Struct. Comput. Sci. 10, 6 (2000), 665–717. http://journals.cambridge.org/action/displayAbstract?aid=71051

work page 2000

[10] [10]

Stefan Banach. 1922. Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales. Fundamenta Mathematicae 3, 1 (1922), 133–181

work page 1922

[11] [11]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy (LIPIcs, Vol. 55), Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi (Eds.). Schloss...

work page doi:10.4230/lipics.icalp.2016.107 2016

[12] [12]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 , Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 90–101. https: //doi.org/10.1145/1...

work page doi:10.1145/1480881.1480894 2009

[13] [13]

Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. IACR Cryptol. ePrint Arch. (2004), 331. http://eprint.iacr.org/2004/331

work page 2004

[14] [14]

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8, 4 (2012). https://doi.org/10. 2168/LMCS-8(4:1)2012

work page 2012

[15] [15]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Note...

work page doi:10.1007/978-3-642- 2014

[16] [16]

Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

work page

[17] [17]

In10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK (LIPIcs, Vol

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK (LIPIcs, Vol. 337) , Maribel Fernández (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2:1–2:20. https: //doi.org/10.423...

work page doi:10.4230/lipics.fscd.2025.2 2025

[18] [18]

Francesco Dagnino and Fabio Pasquali. 2022. Logical Foundations of Quantitative Equality. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , Christel Baier and Dana Fisman (Eds.). ACM, 16:1–16:13. https://doi.org/10.1145/3531130.3533337

work page doi:10.1145/3531130.3533337 2022

[19] [19]

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. 2017. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 545–556. https://doi.org/1...

work page doi:10.1145/3009837.3009890 2017

[20] [20]

de Vink and Jan J

Erik P. de Vink and Jan J. M. M. Rutten. 1999. Bisimulation for Probabilistic Transition Systems: A Coalgebraic Approach. Theor. Comput. Sci. 221, 1-2 (1999), 271–293. https://doi.org/10.1016/S0304-3975(99)00035-3

work page doi:10.1016/s0304-3975(99)00035-3 1999

[21] [21]

Desharnais, V

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. 2000. Approximation of Labeled Markov Processes. In Proceedings of the Fifteenth Annual IEEE Symposium On Logic In Computer Science . IEEE Computer Society Press, 95–106

work page 2000

[22] [22]

Orchard, Flavien Breuvart, and Tarmo Uustalu

Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining effects and coeffects via grading. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 476–489. h...

work page doi:10.1145/2951913.2951939 2016

[23] [23]

Haselwarter, Joseph Tassarotti, and Lars Birkedal

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8, POPL (2024), 753–784. https://doi.org/10.1145/3632868

work page doi:10.1145/3632868 2024

[24] [24]

Wagner, John Kelsey, and Bruce Schneier

Chris Hall, David A. Wagner, John Kelsey, and Bruce Schneier. 1998. Building PRFs from PRPs. In Advances in Cryptology - CRYPTO ’98, 18th Annual International Cryptology Conference, Santa Barbara, California, USA, August 23-27, 1998, Proceedings (Lecture Notes in Computer Science, Vol. 1462) , Hugo Krawczyk (Ed.). Springer, 370–389. https://doi.org/10.100...

work page doi:10.1007/bfb0055742 1998

[25] [25]

Alessandro Giacalone Chi-Chang Jou and Scott A. Smolka. 1994. Algebraic Reasoning for Probabilistic Concurrent Systems. In PROCOMET. North Holland, 443–458

work page 1994

[26] [26]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162–178. https://doi.org/10.1016/0022- 0000(85)90012-1

work page doi:10.1016/0022- 1985

[27] [27]

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. 2022. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , Christel Baier and Dana Fisman (Eds.). ACM, 42:1–42:13. https: //doi.org/...

work page doi:10.1145/3531130.3533359 2022

[28] [28]

Kim Guldstrand Larsen and Arne Skou. 1991. Bisimulation through Probabilistic Testing. Information and Computation 94, 1 (1991), 1–28

work page 1991

[29] [29]

William F. Lawvere. 1973. Metric spaces, generalized logic, and closed categories. In Seminario Mat. e. Fis. di Milano , Vol. 43. Springer, 135–166

work page 1973

[30] [30]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2016. Quantitative Algebraic Reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016 , Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 700–709. https://doi.org/10.1145/2933575.2934518 , Vol. 1, No. 1, A...

work page doi:10.1145/2933575.2934518 2016

[31] [31]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2018. Free complete Wasserstein algebras. Log. Methods Comput. Sci. 14, 3 (2018). https://doi.org/10.23638/LMCS-14(3:19)2018

work page doi:10.23638/lmcs-14(3:19)2018 2018

[32] [32]

Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. 2021. Fixed-Points for Quantitative Equational Logics. In LICS. IEEE, 1–13

work page 2021

[33] [33]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems . Springer. https://doi.org/10.1007/B138392

work page doi:10.1007/b138392 2005

[34] [34]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18, 3 (1996), 325–353. https://doi.org/10.1145/229542.229547

work page doi:10.1145/229542.229547 1996

[35] [35]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 672–681. https://doi.o...

work page doi:10.1145/2933575.2935317 2016

[36] [36]

Jason Reed and Benjamin C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 , Paul Hudak and Stephanie Weirich (Eds.). ACM, 157–168. https: //doi.org/10.1145/1863543.1863568

work page doi:10.1145/1863543.1863568 2010

[37] [37]

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . https: //homotopytypetheory.org/book, Institute for Advanced Study

work page 2013

[38] [38]

Franck van Breugel. 2005. A Behavioural Pseudometric for Metric Labelled Transition Systems. In CONCUR (Lecture Notes in Computer Science, Vol. 3653) . Springer, 141–155

work page 2005

[39] [39]

Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. 2005. An Accessible Approach to Behavioural Pseudometrics. In ICALP (Lecture Notes in Computer Science, Vol. 3580) . Springer, 1018–1030

work page 2005

[40] [40]

Franck van Breugel and James Worrell. 2005. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331, 1 (2005), 115–142. , Vol. 1, No. 1, Article . Publication date: July 2025. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability 29 A OMITTED PROOFS OF SECTION 2 We start by reviewing some ...

work page 2005

[41] [41]

Observe that any Δ can always be described as the sum Δ = Δ1 + 𝑟 Δ2, for appropriate Δ1, Δ2. By inductive hypothesis, then the following is derivable: Γ1, Δ1, Γ′ 1 ⊢ 𝑡 : 𝐵 ⊸𝑝 𝐴 Γ2, Δ2, Γ′ 2 ⊢ 𝑢 : 𝐵 (Γ1, Δ1, Γ′ 1 ) + 𝑟 (Γ′ 2, Δ2, Γ′ 2 ) ⊢ 𝑡 𝑢 : 𝐵 (app) and Γ, Δ, Γ′ = (Γ1, Δ1, Γ′ 1 ) + 𝑟 (Γ′ 2, Δ2, Γ′ 2 ). Case (⊗): Assume Γ, Γ′ ⊢ ( 𝑡, 𝑢) : 𝐴 𝑟 ⊗𝑠𝐵 was deri...

work page

[42] [42]

Case (fix): Assume Γ, Γ′ ⊢ fix 𝑥 .𝑡 : 𝐴 was derived with an application of (fix) and that 𝑥 ∉ Δ (otherwise apply 𝛼-renaming to 𝑡)

By inductive hypothesis, then the following is derivable: Γ1, Δ, Γ′ 1 ⊢ 𝑡 : D𝐴 Γ2, Δ, Γ′ 2 ⊢ 𝑢 : D𝐴 𝑝 ∈ ( 0, 1) 𝑝 (Γ1, Δ, Γ′ 1 ) + ( 1 − 𝑝) (Γ2, Δ, Γ′ 2 ) ⊢ 𝑡 ⊕𝑝 𝑢 : D𝐴 (⊕𝑝 ) and Γ, Δ, Γ′ = 𝑝 (Γ1, Δ, Γ′ 1 ) + ( 1 − 𝑝) (Γ2, Δ, Γ′ 2 ). Case (fix): Assume Γ, Γ′ ⊢ fix 𝑥 .𝑡 : 𝐴 was derived with an application of (fix) and that 𝑥 ∉ Δ (otherwise apply 𝛼-renaming...

work page 2025

[43] [43]

Then from the sub-derivations of Γ1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 and Γ′ 1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 occurring above, by Lemma 5.7, we , Vol

Let Γ∞ be the version of Γ where all sensitivities are set to ∞. Then from the sub-derivations of Γ1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 and Γ′ 1 ⊢ 𝑡 : 𝐴 ⊸𝑟 𝐵 occurring above, by Lemma 5.7, we , Vol. 1, No. 1, Article . Publication date: July 2025. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability 41 obtain new derivations such that the fol...

work page 2025