Pith. sign in

REVIEW 2 major objections 4 minor 46 references

Every type in a cost-aware dependent type theory already contains a potential function, so every program automatically conserves amortized cost while preserving abstraction.

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

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

T0 review · grok-4.5

2026-07-13 06:35 UTC pith:NBHIUQD7

load-bearing objection Clean, mechanized unification of physicist and banker amortization inside Calf; the fracture-gluing for cost algebras and the certifying Giralf embedding are the real advances. the 2 major comments →

arxiv 2607.08547 v2 pith:NBHIUQD7 submitted 2026-07-09 cs.PL cs.DS

Potential Functions as Types

Harrison Grodin (1) , Ethan Chu (1) , Runming Li (1) , Jan Hoffmann (1) , Robert Harper (1) ((1) Carnegie Mellon University) This is my paper
classification cs.PL cs.DS
keywords amortized analysispotential functionsabstraction functionsdependent type theorycost analysiscredits and debitssubstructural typesAARA
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Amortized analysis has long lived in two camps: the physicist's potential functions, which are natural for hand proofs in dependent type theory, and the banker's credits, which are natural for automatic inference in substructural type systems. This paper unifies them inside Calf, a dependent type theory with cost. It proves a fracture-and-gluing theorem showing that every computation type is exactly a concrete type, an abstract type, and a cost-aware abstraction homomorphism that can emit potential. Consequently every map between such types must both preserve the abstract interface and conserve potential. Credits and debits are then defined as ordinary type operators inside the same theory, yielding Giralf, a graded substructural language that sits as a well-behaved sub-language of Calf. An adapted linear-programming inference algorithm turns a useful fragment of Calf programs into Giralf certificates that automatically supply amortized bounds. The result is a single setting in which manual amortized proofs, modular interfaces, and automatic resource analysis coexist.

Core claim

Every computation type is equivalent to a triple consisting of a concrete type, an abstract type, and an abstraction homomorphism that may charge cost; that cost is precisely the potential stored in the type. Therefore every homomorphism between computation types automatically carries both a proof that abstraction is preserved and a proof that potential is conserved, recovering the physicist's amortized-analysis inequality by construction.

What carries the argument

Fracture and gluing of the universe of cost algebras (Theorem 2.15): the equivalence C ≃ Σ A•:C• Σ A◦:C◦ (A• ⊸ A◦) that turns every type into a fused abstraction-plus-potential function and forces every program to be a lax square that conserves potential.

Load-bearing premise

Computation types must be cost algebras whose charge operation is an action of a commutative cost monoid, and the concrete modality must preserve the limits needed for the gluing construction; if either fails the equivalence collapses.

What would settle it

Exhibit a cost monoid that is non-commutative, or a computation type whose charge operation is not a monoid action, for which the claimed fracture-and-gluing equivalence between C and the sum of concrete types, abstract types and abstraction homomorphisms fails to hold.

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

If this is right

  • Amortized cost interfaces become ordinary abstract-phase specifications that clients can use without seeing implementation potential.
  • Credits and debits are ordinary type formers inside dependent type theory, so banker's-style data structures can be written and verified directly in Calf.
  • Giralf programs are genuine Calf terms; therefore automatic AARA-style bounds produce certificates that are checkable inside the same dependent type theory.
  • Common algorithms such as insertion sort receive automatic triangular amortized bounds that are still fully formalized as Calf programs.

Where Pith is reading between the lines

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

  • The same fracture-and-gluing pattern should extend, with only local changes, to other monoidal effects beyond cost, giving modular interfaces for time, space, and probabilistic resources simultaneously.
  • Because credits are companions of cost, the construction supplies a semantic explanation of why resource-polymorphic recursion works: the changing linear coefficient is just the residual potential after a debit is taken.
  • Persistent amortized data structures that rely on laziness may be reachable by replacing the present cost algebra with a delay monad that still admits a lex concrete modality.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 4 minor

Summary. The paper unifies the physicist’s and banker’s views of amortized analysis inside Calf. It proves a fracture-and-gluing theorem for the universe of computation types (Theorem 2.15): every cost algebra A is equivalent to a concrete type, an abstract type, and an abstraction homomorphism A• ⊸ A◦ that may emit cost (potential). Consequently every homomorphism automatically carries both abstraction preservation and conservation of potential. Credits ▷c A and debits ◁c A are defined synthetically from the same construction; Giralf is introduced as a graded substructural dependent type theory whose programs interpret as a zero-abstract-cost sub-language of Calf; an LP-based inference algorithm (adapted from AARA/RaML) produces certifying Giralf terms for a limited class of Calf programs. Central constructions and the Giralf semantics are mechanized in Cubical Agda.

Significance. If the results hold, the paper supplies a single dependent type theory in which manual amortized verification (via potential) and automated banker’s-style inference (via credits) coexist, with modularity enforced by a synthetic phase distinction. The mechanized fracture-and-gluing theorem for cost algebras, the credit/debit adjunction, the embedding of AARA-style types as Potential(Φ), and the certifying inference pipeline are concrete, reusable contributions. The work therefore advances both the foundations of cost-aware type theory and the practical integration of AARA techniques into a full dependent setting.

major comments (2)
  1. The inference algorithm of §5.3 is restricted to the skeletal grammar ⊤ | A+B | A×B | List(FX) and produces only polynomial (linear/quadratic) credit annotations. The abstract and introduction claim that the algorithm “automates the cost analysis of common algorithms in Calf.” Either the claim should be qualified to the fragment actually handled, or the manuscript should supply at least one non-trivial example outside that fragment (e.g., the red-black or splay-tree credit schemes of §4.3) together with evidence that the LP encoding still succeeds.
  2. Theorem 5.7 and the subsequent soundness theorem for AARA (Theorem 5.8) are stated only for the positive fragment of AARA types. Negative types (products, powers, debits) appear in Giralf and are essential to the claim that Giralf generalizes AARA, yet their potential semantics are left open (Remark 5.6). A short argument or counter-example clarifying the status of negative types would make the generalization claim precise.
minor comments (4)
  1. Definition 2.11 introduces cost algebras with a monoid action of a commutative cost monoid; the necessity of commutativity is acknowledged only later (Remark 4.2 and §7). A forward pointer at the definition would help readers who expect non-commutative high-water-mark models.
  2. The sealing monad S of §3.2 is introduced as a user-specified comma object rather than an effect; the interaction with the fracture-and-gluing equivalence (Theorem 2.15) is only sketched. A one-sentence statement that S preserves the required pullbacks would close the gap.
  3. Several examples (batched queues, insertion sort, snoc) are repeated across the physicist’s and banker’s sections. Cross-references of the form “cf. Example 2.20 / 4.16” would reduce redundancy without lengthening the text.
  4. The data-availability statement notes that the Agda development replaces the inequality structure of prior Calf work by equality “as an approximation.” A brief remark on which theorems remain valid under genuine inequality would be useful for readers who wish to reuse the library.

Circularity Check

0 steps flagged

No significant circularity: potential is defined as the cost of the abstraction homomorphism, conservation follows from gluing, and self-citations are to independently mechanized prior work.

full rationale

The paper's central claim (Theorem 2.15) is a constructive fracture-and-gluing equivalence for the universe of cost algebras: every computation type is assembled from a concrete type, an abstract type, and an abstraction homomorphism that may emit cost (potential). Homomorphisms between such types therefore contain, by the universal property of the glue, both an abstraction-preserving map and a conservation-of-potential inequality. Credits (Definition 4.1) and Potential (Definition 2.21) are defined directly from that same homomorphism; the banker's operators and the Giralf semantics are then interpreted inside Calf by construction. There are no fitted parameters, no empirical normalizations, and no uniqueness theorems imported solely by self-citation. The heavy citations to prior Calf/AFAT work (Niu et al. 2022, Grodin & Harper 2024, Grodin et al. 2026) supply independently mechanized foundations that are used as black boxes; the present paper re-proves the new fracture theorem for cost algebras and marks the key results as mechanized in Cubical Agda. The only mild self-referential flavor is the definitional identification of potential with the cost of the abstraction map, which is an intentional synthetic design choice rather than a circular prediction. Score 1 reflects ordinary self-citation of prior mechanized results without load-bearing circular reduction of the main claim.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 3 invented entities

The paper rests on standard univalent type theory, the modalities of Rijke et al., the existing Calf cost effect and phase distinction, and the algebraic structure of AARA potential functions. No free parameters are fitted; the only domain assumptions are the cost-algebra presentation of computation types and commutativity of the cost monoid. Invented entities (Giralf, the credit/debit operators, PFAT) are defined constructively from those ingredients and therefore carry independent formal evidence via the Agda mechanization.

axioms (3)
  • domain assumption Computation types are cost algebras: a preordered value type equipped with a monoid action of a commutative cost monoid (Definition 2.11).
    Required for the concrete modality and for fracture-and-gluing of C; stated explicitly and used throughout Sections 2–5.
  • standard math The abstract phase proposition abs and the associated modalities # and (Rijke et al. 2020) form a stable orthogonal factorization system that interacts correctly with the cost effect.
    Background modal type theory; the paper proves the necessary lex and conservativity lemmas for the cost-algebra case.
  • domain assumption Cost monoid is commutative, enabling tensor products and the lifting of charge to homomorphisms.
    Explicitly noted as essential for credits and LNL connectives; non-commutative high-water-mark models are left to future work.
invented entities (3)
  • Potential Functions as Types (PFAT) / Abstraction(α) for cost-algebra homomorphisms independent evidence
    purpose: Package an abstraction-plus-potential homomorphism into a single computation type so that every map automatically conserves potential.
    Defined via the gluing construction of Theorem 2.15; independent evidence is the Agda formalization and the derived conservation squares.
  • Credit operator ▷c A and debit operator ◁c A independent evidence
    purpose: Internalize the banker's view as type formers that emit or assume cost in the abstraction homomorphism.
    Defined synthetically from Abstraction and the sealing monad; lemmas (adjunction, ghostness, save/spend) are proved and mechanized.
  • Giralf graded substructural type theory independent evidence
    purpose: Provide a convenient syntax for credit-carrying programs that is interpreted as a sub-language of Calf and supports LP-based inference.
    Syntax, typing rules, and resource-aware semantics are given; soundness of the AARA embedding follows from the Kripke semantics of Calf.

pith-pipeline@v1.1.0-grok45 · 33483 in / 2646 out tokens · 27627 ms · 2026-07-13T06:35:01.637197+00:00 · methodology

0 comments
read the original abstract

Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to automated inference in substructural type theory using type-level credit annotations. In this work, we synthesize these perspectives in Calf, a dependent type theory cost verification. From the physicist's view, we present a fracture and gluing theorem that renders every type as containing a fusion of an abstraction function and a potential function. By construction, every program between two such types must preserve abstraction, to facilitate modularity of behavior, and conserve potential, to facilitate modularity of cost. Incorporating the banker's view, we synthetically construct type operators for credits and debits. We then define Giralf, a graded substructural dependent type theory for programming with credits and debits, which is semantically interpreted as a sub-language of Calf. Finally, we adapt an inference algorithm to transform a limited class of Calf programs into Giralf counterparts, automating the cost analysis of common algorithms in Calf.

Figures

Figures reproduced from arXiv: 2607.08547 by Ethan Chu (1), Harrison Grodin (1), Jan Hoffmann (1), Robert Harper (1) ((1) Carnegie Mellon University), Runming Li (1).

Figure 1
Figure 1. Figure 1: The central ideas of this work. (1) We work in Calf [Grodin et al. 2024; Niu et al. 2022], a dependent type theory for cost verification. Within Calf, the conservation of energy principle used the physicist’s view of amortized analysis can be packaged as a lax commutative square [Grodin and Harper 2024]. (2) We make use of the insights of Grodin et al. [2026] who achieve modularity in (univalent) dependent… view at source ↗
Figure 2
Figure 2. Figure 2: The potential-based semantics of AARA types [ [PITH_FULL_IMAGE:figures/full_fig_p020_2.png] view at source ↗

Review history (2 revisions) →

discussion (0)

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

Reference graph

Works this paper leans on

46 extracted references · 3 linked inside Pith

  1. [1]

    InFoundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Bart Jacobs and Christof Löding (Eds.)

    Dependent Types and Fibred Computational Effects. InFoundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Bart Jacobs and Christof Löding (Eds.). Springer, Berlin, Heidelberg, 36–54. https://doi.org/10.1007/978-3-662-49630-5_3 Robert Atkey

    doi:10.1007/978-3-662-49630-5_3

  2. [2]

    https://doi.org/10.2168/LMCS-7(2:17)2011 Robert Atkey

    Amortised Resource Analysis with Separation Logic.Logical Methods in Computer ScienceVolume 7, Issue 2 (June 2011). https://doi.org/10.2168/LMCS-7(2:17)2011 Robert Atkey

    doi:10.2168/lmcs-7(2:17)2011 2011

  3. [3]

    InProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14)

    From Parametricity to Conservation Laws, via Noether’s Theorem. InProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA, 491–502. https://doi.org/10.1145/2535838.2535867 P. N. Benton

    doi:10.1145/2535838.2535867

  4. [4]

    InComputer Science Logic (Lecture Notes in Computer Science), Leszek Pacholski and Jerzy Tiuryn (Eds.)

    A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models. InComputer Science Logic (Lecture Notes in Computer Science), Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer, Berlin, Heidelberg, 121–135. https: //doi.org/10.1007/BFb0022251 F. Warren Burton

    doi:10.1007/bfb0022251

  5. [5]

    An Efficient Functional Implementation of FIFO Queues.Inform. Process. Lett.14, 5 (July 1982), 205–206. https://doi.org/10.1016/0020-0190(82)90015-1 Joseph W. Cutler, Daniel R. Licata, and Norman Danner

    doi:10.1016/0020-0190(82)90015-1 1982

  6. [6]

    Proceedings of the ACM on Programming Languages4, ICFP (Aug

    Denotational Recurrence Extraction for Amortized Analysis. Proceedings of the ACM on Programming Languages4, ICFP (Aug. 2020), 97:1–97:29. https://doi.org/10.1145/3408979 Nils Anders Danielsson

    doi:10.1145/3408979 2020

  7. [7]

    ACM SIGPLAN Notices43, 1 (Jan

    Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. ACM SIGPLAN Notices43, 1 (Jan. 2008), 133–144. https://doi.org/10.1145/1328897.1328457 Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar

    doi:10.1145/1328897.1328457 2008

  8. [8]

    In2021 IEEE 34th Computer Security Foundations Symposium (CSF)

    Resource-Aware Session Types for Digital Contracts. In2021 IEEE 34th Computer Security Foundations Symposium (CSF). 1–16. https://doi.org/10.1109/ CSF51468.2021.00004 Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson

    arXiv 2021

  9. [9]

    InComputer Science Logic (Lecture Notes in Computer Science), Erich Grädel and Reinhard Kahle (Eds.)

    Enriching an Effect Calculus with Linear Types. InComputer Science Logic (Lecture Notes in Computer Science), Erich Grädel and Reinhard Kahle (Eds.). Springer, Berlin, Heidelberg, 240–254. https://doi.org/10.1007/978-3-642-04027-6_19 Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson

    doi:10.1007/978-3-642-04027-6_19

  10. [10]

    https://doi.org/10.1093/logcom/exs025 Marco Grandis and Robert Paré

    The Enriched Effect Calculus: Syntax and Semantics.Journal of Logic and Computation24, 3 (June 2014), 615–654. https://doi.org/10.1093/logcom/exs025 Marco Grandis and Robert Paré

    doi:10.1093/logcom/exs025 2014

  11. [11]

    https://www.numdam.org/item/?id=CTGDC_2004__45_3_193_0 David Gries

    Adjoint for Double Categories.Cahiers de Topologie et Géométrie Différentielle Catégoriques45, 3 (2004), 193–240. https://www.numdam.org/item/?id=CTGDC_2004__45_3_193_0 David Gries. 1989.The Science of Programming. Springer New York. Harrison Grodin and Robert Harper

    2004

  12. [12]

    Amortized Analysis via Coalgebra.Electronic Notes in Theoretical Informatics and Computer ScienceVolume 4 - Proceedings of MFPS XL (Dec. 2024). https://doi.org/10.46298/entics.14797 Harrison Grodin, Runming Li, and Robert Harper

    doi:10.46298/entics.14797 2024

  13. [13]

    2026), 31:895–31:922

    Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory.Proceedings of the ACM on Programming Languages10, POPL (Jan. 2026), 31:895–31:922. https://doi.org/10.1145/3776673 Harrison Grodin, Yue Niu, Jonathan Sterling, and Robert Harper

    doi:10.1145/3776673 2026

  14. [14]

    2024), 10:273–10:301

    Decalf: A Directed, Effectful Cost-Aware Logical Framework.Proceedings of the ACM on Programming Languages8, POPL (Jan. 2024), 10:273–10:301. https://doi.org/10. 1145/3632852 Jessie Grosen, David M. Kahn, and Jan Hoffmann

    2024

  15. [15]

    In2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

    Automatic Amortized Resource Analysis with Regular Recursive Types. In2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–14. https://doi.org/10.1109/ LICS56636.2023.10175720 Leo J. Guibas and Robert Sedgewick

    arXiv 2023

  16. [16]

    In19th Annual Symposium on Foundations of Computer Science (Sfcs 1978)

    A Dichromatic Framework for Balanced Trees. In19th Annual Symposium on Foundations of Computer Science (Sfcs 1978). 8–21. https://doi.org/10.1109/SFCS.1978.3 C. A. R. Hoare

    doi:10.1109/sfcs.1978.3 1978

  17. [17]

    1972), 271–281

    Proof of Correctness of Data Representations.Acta Informatica1, 4 (Dec. 1972), 271–281. https: //doi.org/10.1007/BF00289507 Potential Functions as Types 27 Jan Hoffmann, Klaus Aehlig, and Martin Hofmann

    doi:10.1007/bf00289507 1972

  18. [18]

    InProceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11)

    Multivariate Amortized Resource Analysis. InProceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA, 357–370. https://doi.org/10.1145/1926385.1926427 Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012a. Multivariate Amortized Resource Analysis.A...

    doi:10.1145/1926385.1926427 2012

  19. [19]

    https://doi.org/10.1017/S0960129521000487 Martin Hofmann and Steffen Jost

    Two Decades of Automatic Amortized Resource Analysis.Mathematical Structures in Computer Science32, 6 (June 2022), 729–759. https://doi.org/10.1017/S0960129521000487 Martin Hofmann and Steffen Jost

    doi:10.1017/s0960129521000487 2022

  20. [20]

    2003), 185–197

    Static Prediction of Heap Space Usage for First-Order Functional Programs.ACM SIGPLAN Notices38, 1 (Jan. 2003), 185–197. https://doi.org/10.1145/640128.604148 Martin Hofmann, Lorenz Leutgeb, David Obwaller, Georg Moser, and Florian Zuleger

    doi:10.1145/640128.604148 2003

  21. [21]

    https: //doi.org/10.1017/S0960129521000232 Robert Hood and Robert Melville

    Type-Based Analysis of Logarithmic Amortised Complexity.Mathematical Structures in Computer Science32, 6 (June 2022), 794–826. https: //doi.org/10.1017/S0960129521000232 Robert Hood and Robert Melville

    doi:10.1017/s0960129521000232 2022

  22. [22]

    Real-Time Queue Operations in Pure LISP.Inform. Process. Lett.13, 2 (Nov. 1981), 50–54. https://doi.org/10.1016/0020-0190(81)90030-2 David M. Kahn and Jan Hoffmann

    doi:10.1016/0020-0190(81)90030-2 1981

  23. [23]

    InFoundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Jean Goubault-Larrecq and Barbara König (Eds.)

    Exponential Automatic Amortized Resource Analysis. InFoundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Jean Goubault-Larrecq and Barbara König (Eds.). Springer International Publishing, Cham, 359–380. https://doi.org/10.1007/978-3-030-45231-5_19 Lukas Kebuladze. 2025.Formally Verified Amortized Cost Analysis o...

    doi:10.1007/978-3-030-45231-5_19 2025

  24. [24]

    https://doi.org/10.1145/2775051.2676969 Paul Blain Levy

    Integrating Linear and Dependent Types.ACM SIGPLAN Notices50, 1 (2015), 17–30. https://doi.org/10.1145/2775051.2676969 Paul Blain Levy. 2003.Call-By-Push-Value: A Functional/Imperative Synthesis. Springer Netherlands, Dordrecht. https: //doi.org/10.1007/978-94-007-0954-6 Runming Li and Robert Harper

    doi:10.1145/2775051.2676969 2015

  25. [25]

    https://doi.org/10.48550/arXiv.2504.12464 arXiv:2504.12464 [cs] Anton Lorenzen

    Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. https://doi.org/10.48550/arXiv.2504.12464 arXiv:2504.12464 [cs] Anton Lorenzen

    Pith/arXiv arXiv doi:10.48550/arxiv.2504.12464

  26. [26]

    https://doi.org/arXiv:2605.09411 Lambert Meertens

    Persistent Amortised Analysis, Operationally. https://doi.org/arXiv:2605.09411 Lambert Meertens

    Pith/arXiv arXiv

  27. [27]

    1992), 413–424

    Paramorphisms.Formal Aspects of Computing4, 5 (Sept. 1992), 413–424. https://doi.org/10.1007/ BF01211391 Glen Mével, Jacques-Henri Jourdan, and François Pottier

    1992

  28. [28]

    InProgramming Languages and Systems, Luís Caires (Ed.)

    Time Credits and Time Receipts in Iris. InProgramming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham, 3–29. https://doi.org/10.1007/978-3- 030-17184-1_1 Tobias Nipkow and Hauke Brinkop

    doi:10.1007/978-3-

  29. [29]

    https://doi.org/10.1007/s10817-018-9459-3 Yue Niu and Robert Harper

    Amortized Complexity Verified.Journal of Automated Reasoning62, 3 (March 2019), 367–391. https://doi.org/10.1007/s10817-018-9459-3 Yue Niu and Robert Harper

    doi:10.1007/s10817-018-9459-3 2019

  30. [30]

    https://doi.org/10.48550/arXiv

    A Metalanguage for Cost-Aware Denotational Semantics. https://doi.org/10.48550/arXiv. 2209.12669 arXiv:2209.12669 [cs] Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper

    Pith/arXiv arXiv doi:10.48550/arxiv

  31. [31]

    2022), 9:1–9:31

    A Cost-Aware Logical Framework.Proceedings of the ACM on Programming Languages6, POPL (Jan. 2022), 9:1–9:31. https://doi.org/10.1145/3498670 Ulf Norell

    doi:10.1145/3498670 2022

  32. [32]

    InProceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09)

    Dependently Typed Programming in Agda. InProceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09). Association for Computing Machinery, New York, NY, USA, 1–2. https://doi.org/10.1145/1481861.1481862 Chris Okasaki. 1999.Purely Functional Data Structures. Cambridge University Press. Pierre-Marie Pédrot and Nic...

    doi:10.1145/1481861.1481862 1999

  33. [33]

    2019), 58:1–58:28

    The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects.Proceedings of the ACM on Programming Languages4, POPL (Dec. 2019), 58:1–58:28. https://doi.org/10.1145/ 3371126 Long Pham, Yue Niu, Nathan Glover, Feras Saad, and Jan Hoffmann

    2019

  34. [34]

    2025), 409:3811–409:3840

    Integrating Resource Analyses via Resource Decomposition.Proceedings of the ACM on Programming Languages9, OOPSLA2 (Oct. 2025), 409:3811–409:3840. https://doi.org/10.1145/3763798 28 Harrison Grodin, Ethan Chu, Runming Li, Jan Hoffmann, and Robert Harper François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével

    doi:10.1145/3763798 2025

  35. [35]

    2024), 50:1482–50:1508

    Thunks and Debits in Separation Logic with Time Credits.Proceedings of the ACM on Programming Languages8, POPL (Jan. 2024), 50:1482–50:1508. https://doi.org/10.1145/3632892 Vineet Rajani. 2020.A Type-Theory for Higher-Order Amortized Analysis. doctoralThesis. Saarländische Universitäts- und Landesbibliothek. https://doi.org/10.22028/D291-30877 Vineet Raja...

    doi:10.1145/3632892 2024

  36. [36]

    ACM Program

    A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs.Proc. ACM Program. Lang.8, OOPSLA2 (Oct. 2024), 285:389–285:414. https://doi.org/10.1145/3689725 Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann

    doi:10.1145/3689725 2024

  37. [37]

    2021), 27:1–27:28

    A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis.Proceedings of the ACM on Programming Languages5, POPL (Jan. 2021), 27:1–27:28. https: //doi.org/10.1145/3434308 John C. Reynolds

    doi:10.1145/3434308 2021

  38. [38]

    InInformation Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R

    Types, Abstraction, and Parametric Polymorphism. InInformation Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R. E. A. Mason (Ed.). North-Holland/IFIP, 513–523. https://doi.org/10.1007/3-540-55511-0_1 Emily Riehl and Michael Shulman

    doi:10.1007/3-540-55511-0_1 1983

  39. [39]

    2017), 147–224

    A Type Theory for Synthetic ∞-Categories.Higher Structures1, 1 (Dec. 2017), 147–224. https://doi.org/10.21136/HS.2017.06 Egbert Rijke, Michael Shulman, and Bas Spitters

    doi:10.21136/hs.2017.06 2017

  40. [40]

    Modalities in Homotopy Type Theory.Logical Methods in Computer ScienceVolume 16, Issue 1 (Jan. 2020). https://doi.org/10.23638/LMCS-16(1:2)2020 Daniel D. Sleator and Robert E. Tarjan. 1985a. Amortized Efficiency of List Update and Paging Rules.Commun. ACM28, 2 (Feb. 1985), 202–208. https://doi.org/10.1145/2786.2793 Daniel Dominic Sleator and Robert Endre ...

    doi:10.23638/lmcs-16(1:2)2020 2020

  41. [41]

    Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM68, 6 (Oct. 2021), 41:1–41:47. https://doi.org/10.1145/3474834 Ross Street

    doi:10.1145/3474834 2021

  42. [42]

    InCategory Seminar, Gregory M

    Fibrations and Yoneda’s Lemma in a 2-Category. InCategory Seminar, Gregory M. Kelly (Ed.). Springer, Berlin, Heidelberg, 104–133. https://doi.org/10.1007/BFb0063102 Robert Endre Tarjan

    doi:10.1007/bfb0063102

  43. [43]

    https://doi.org/10.1137/0606031 The Univalent Foundations Program

    Amortized Computational Complexity.SIAM Journal on Algebraic Discrete Methods6, 2 (April 1985), 306–318. https://doi.org/10.1137/0606031 The Univalent Foundations Program. 2013.Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program. Matthijs Vákár. 2017.In Search of Effectful Dependent Types. http://purl.org/dc/dcmitype/...

    doi:10.1137/0606031 1985

  44. [44]

    In Proceedings of the 17th ACM SIGPLAN International Haskell Symposium (Haskell 2024)

    Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl). In Proceedings of the 17th ACM SIGPLAN International Haskell Symposium (Haskell 2024). Association for Computing Machinery, New York, NY, USA, 97–108. https://doi.org/10.1145/3677999.3678282 Andrea Vezzosi, Anders Mörtberg, and Andreas Abel

    doi:10.1145/3677999.3678282 2024

  45. [45]

    https://doi.org/10.1145/3341691 Han Xu and Di Wang

    Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.Proceedings of the ACM on Programming Languages3, ICFP (July 2019), 87:1–87:29. https://doi.org/10.1145/3341691 Han Xu and Di Wang

    doi:10.1145/3341691 2019

  46. [46]

    InProgramming Languages and Systems, Robbert Krebbers (Ed.)

    Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs. InProgramming Languages and Systems, Robbert Krebbers (Ed.). Springer Nature Switzerland, Cham, 362–391. https://doi.org/10.1007/978-3-032-22723-2_13

    doi:10.1007/978-3-032-22723-2_13