LFPL: Revisited and Mechanized

Jan Hoffmann; Nathaniel Glover

arxiv: 2605.12893 · v2 · pith:3OY76YUAnew · submitted 2026-05-13 · 💻 cs.PL · cs.CC· cs.LO

LFPL: Revisited and Mechanized

Nathaniel Glover , Jan Hoffmann This is my paper

Pith reviewed 2026-05-20 21:38 UTC · model grok-4.3

classification 💻 cs.PL cs.CCcs.LO

keywords LFPLpolynomial timemechanized metatheorysoundnesscompletenesslinear typescost boundsTuring machine simulation

0 comments

The pith

LFPL programs are proven to compute exactly the polynomial-time functions through mechanized soundness and completeness arguments.

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

The paper gives a self-contained modern presentation of LFPL, the functional language whose affine type system was meant to guarantee polynomial running time. It mechanizes the full metatheory in the Istari assistant, adapting an existing technique to produce explicit polynomial cost bounds for an extended version called LFPL+. It also mechanizes completeness by showing that any polynomial-time Turing machine can be simulated inside LFPL using a new stack-like structure built only from first-class functions and lists. This establishes that the language is both sound for resource bounds and complete for all polynomial-time computation while supporting natural programming features such as nested recursion.

Core claim

We mechanize the soundness of LFPL+ by adapting the Aehlig-Schwichtenberg technique to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. We mechanize completeness by showing that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists, using a novel stack-like data structure implemented with first-class functions and lists that simplifies the core argument.

What carries the argument

A novel stack-like data structure implemented with first-class functions and lists that simulates Turing-machine tapes while obeying LFPL's linear restrictions on functions and lists.

Load-bearing premise

The novel stack-like data structure built from first-class functions and lists correctly implements the simulation of polynomial-time Turing machines while respecting the restricted linear functions and lists required by LFPL.

What would settle it

An explicit polynomial-time Turing machine that cannot be encoded as an LFPL program using the described stack-like data structure, or a concrete LFPL+ term whose measured execution cost exceeds every polynomial derived by the adapted bounding technique.

read the original abstract

Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural programming style, including nested recursion, and has inspired the development of type systems for automatic cost analysis, linear dependent type theories, and efficient memory management in functional programming languages. Despite its prominence, there does not exist a self-contained presentation, let alone a full mechanization, of LFPL and its core metatheory. This article presents a modern account and mechanization of LFPL and its metatheory with the goal of being self-contained and accessible while streamlining the strongest-known soundness and completeness results. The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists. The mechanization includes the full soundness and completeness proofs, and serves as one of the first case studies of mechanized metatheory in the recently developed proof assistant Istari.

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

This paper delivers a useful mechanization of LFPL metatheory in Istari with explicit polynomial bounds and a cleaner stack-based completeness argument.

read the letter

The main takeaway is that Glover and Hoffmann have produced a self-contained mechanization of LFPL in Istari that covers both soundness and completeness for the polynomial-time characterization. They adapt the Aehlig-Schwichtenberg technique to build explicit cost bounds under a big-step semantics for an extended version they call LFPL+, and they replace the original completeness construction with a simpler stack-like structure made from first-class functions and lists that still fits the affine typing discipline. The Istari proofs are the clearest addition here because they give machine-checked evidence rather than just another pen-and-paper argument. That kind of artifact is worth having when people want to reuse the core for other resource-aware systems. The presentation is also more accessible than the 1999 and 2002 sources, which helps anyone trying to build on the work without chasing down scattered details. On the weaker side, the soundness result is stated for LFPL+ rather than the exact original language, so readers who need the strict original formulation will still have to do some translation. The completeness argument keeps the same overall shape as Hofmann's earlier proof and mainly improves the central data structure, so it is an incremental rather than revolutionary change. Nothing in the abstract or the described proof strategy looks circular or dependent on fitted parameters. This is the sort of paper that would be useful to anyone working on linear dependent types, automatic cost analysis, or mechanized metatheory for complexity bounds. It is solid enough to send for peer review; the mechanization itself supplies the kind of reproducible evidence that referees can check directly.

Referee Report

0 major / 3 minor

Summary. The paper presents a modern self-contained account of LFPL (Hofmann 1999) and its metatheory, together with a full mechanization in the Istari proof assistant. Soundness is established for the extension LFPL+ by adapting the Aehlig-Schwichtenberg technique to derive explicit polynomial cost bounds relative to a big-step semantics. Completeness is shown by constructing a simulation of polynomial-time Turing machines inside LFPL that uses only the language's restricted affine functions and lists; the simulation is realized via a novel stack-like data structure built from first-class functions and lists, simplifying the original Hofmann argument while preserving the type discipline.

Significance. If the mechanization is faithful, the work supplies independent machine-checked evidence for both the soundness and completeness directions, which is a substantial strengthening of the foundational results in implicit computational complexity. The explicit polynomial bounds, the streamlined completeness argument, and the Istari case study are all positive contributions that could support further research on linear dependent types, automatic cost analysis, and resource-aware functional programming.

minor comments (3)

The abstract and introduction should explicitly list the additional constructs that distinguish LFPL+ from the original LFPL, so that readers can immediately see which features are covered by the new soundness argument.
In the completeness section, a short concrete example of the novel stack-like data structure (showing a few operations and their typing) would make the simplification of the Hofmann argument easier to follow without requiring the reader to reconstruct the implementation from the prose description.
The mechanization overview would benefit from a brief statement of the total number of lines or key lemmas proved, to give a sense of the scale of the Istari development.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work and for recommending minor revision. We appreciate the recognition of the self-contained mechanization, the adapted soundness proof, and the simplified completeness argument via the novel stack-like data structure.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper mechanizes both soundness (via adaptation of the external Aehlig-Schwichtenberg technique to produce explicit polynomial cost bounds for LFPL+) and completeness (via a novel stack-like data structure built from first-class functions and lists that simulates polynomial-time TMs while respecting LFPL's affine typing). These steps are independent constructions verified by machine-checked Istari proofs rather than self-definitional reductions, fitted parameters renamed as predictions, or load-bearing self-citations. The completeness argument follows the structure of Hofmann (2002) but simplifies it with new components that are type-checked against the language restrictions, providing external falsifiability. No equation or claim reduces to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper rests on standard mathematical facts about polynomials and computation; no free parameters, invented entities, or ad-hoc axioms are introduced beyond the usual background of complexity theory and type systems.

axioms (1)

standard math Standard properties of polynomial functions and big-step operational semantics hold for bounding computation cost.
Invoked when constructing explicit polynomials that bound the cost of LFPL+ expressions.

pith-pipeline@v0.9.0 · 5791 in / 1253 out tokens · 85237 ms · 2026-05-20T21:38:30.015312+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 washburn_uniqueness_aczel unclear

?

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

The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics.
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

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

The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists.

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.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

[1]

A Fresh Look at the lambda-Calculus

1 Beniamino Accattoli. A Fresh Look at the lambda-Calculus. In4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 1:1–1:20. Schloss Dagstuhl – Leibniz- Zentrum für Informatik, June 2019.doi:10.4230/LIPIcs.FSCD.2019.1. 2 Klaus Aehlig and H...

work page doi:10.4230/lipics.fscd.2019.1 2019
[2]

doi:10.1145/232627.232650. 7 G. Bonfante, J. Y. Marion, and J. Y. Moyen. Quasi-interpretations a way to control resources. Theor. Comput. Sci., 412(25):2776–2796, June 2011.doi:10.1016/j.tcs.2011.02.007. 8Karl Crary. The Istari proof assistant.https://istarilogic.org/,

work page doi:10.1145/232627.232650 2011
[3]

10 Ugo Dal Lago and Martin Hofmann

doi:10.1017/S0960129521000505. 10 Ugo Dal Lago and Martin Hofmann. Realizability models and implicit complexity.Theor. Comput. Sci., 412(20):2029–2047, April 2011.doi:10.1016/j.tcs.2010.12.025. 11 Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. Formal proof of polynomial-time complexity with quasi-interpretations. InProceedings o...

work page doi:10.1017/s0960129521000505 2029
[4]

13 Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca

Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2007).doi:10.1016/j.entcs.2008.03.066. 13 Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. An Implicit Char- acterization of PSPACE.ACM Trans. Comput. Logic, 13(2):1–36, April

work page doi:10.1016/j.entcs.2008.03.066 2007
[5]

14 Nathaniel Glover and Jan Hoffmann

doi: 10.1145/2159531.2159540. 14 Nathaniel Glover and Jan Hoffmann. LFPL: Revisited and Mechanized - Source Code of the Mechanization, May

work page doi:10.1145/2159531.2159540
[6]

15 Sylvain Heraud and David Nowak

URL:https://doi.org/10.5281/zenodo.18348213. 15 Sylvain Heraud and David Nowak. A formalization of polytime functions. InProceedings of the Second International Conference on Interactive Theorem Proving, ITP ’11, page 119–134. Springer-Verlag, August

work page doi:10.5281/zenodo.18348213
[7]

Two decades of automatic amortized resource analysis.Math

16 Jan Hoffmann and Steffen Jost. Two decades of automatic amortized resource analysis.Math. Struct. Comput. Sci., 32(6):729–759, March 2022.doi:10.1017/S0960129521000487. 17 Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS 1999, page...

work page doi:10.1017/s0960129521000487 2022
[8]

Glover and J

N. Glover and J. Hoffmann 29 19 Martin Hofmann. The strength of non-size increasing computation. InProceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’02, page 260–269. Association for Computing Machinery, January 2002.doi:10.1145/503272.5 03297. 20 Martin Hofmann. Linear types and non-size-increasing polynom...

work page doi:10.1145/503272.5 2002
[9]

24 Anton Lorenzen, Daan Leijen, and Wouter Swierstra

doi:10.1145/3779031.3779085. 24 Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP2: Fully in-Place Functional Program- ming.Proc. ACM Program. Lang., 7(ICFP):275–304, August 2023.doi:10.1145/3607840. 25 Jean-Yves Marion. Analysing the implicit complexity of programs.Inf. Comput., 183(1):2–18, May 2003.doi:10.1016/S0890-5401(03)00011-7. 26 Jean-Yves Ma...

work page doi:10.1145/3779031.3779085 2023
[10]

Typable Fragments of Polynomial Automatic Amortized Resource Analysis

29 Long Pham and Jan Hoffmann. Typable Fragments of Polynomial Automatic Amortized Resource Analysis. In29th EACSL Annual Conference on Computer Science Logic, CSL 2021, volume 183 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 34:1– 34:19, Dagstuhl, Germany,

work page 2021
[11]

30 Ramyaa Ramyaa and Daniel Leivant

Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi: 10.4230/LIPIcs.CSL.2021.34. 30 Ramyaa Ramyaa and Daniel Leivant. Ramified Corecurrence and Logspace.Electronic Notes in Theoretical Computer Science, 276:247–261, September

work page doi:10.4230/lipics.csl.2021.34 2021
[12]

31 Ulrich Schopp

Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 27.doi:10.1016/j.en tcs.2011.09.025. 31 Ulrich Schopp. Stratified Bounded Affine Logic for Logarithmic Space. InProceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS ’07, pages 411–420. IEEE Computer Society, July 2007.doi:10.1109/LICS.2007....

work page doi:10.1016/j.en 2011

[1] [1]

A Fresh Look at the lambda-Calculus

1 Beniamino Accattoli. A Fresh Look at the lambda-Calculus. In4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 1:1–1:20. Schloss Dagstuhl – Leibniz- Zentrum für Informatik, June 2019.doi:10.4230/LIPIcs.FSCD.2019.1. 2 Klaus Aehlig and H...

work page doi:10.4230/lipics.fscd.2019.1 2019

[2] [2]

doi:10.1145/232627.232650. 7 G. Bonfante, J. Y. Marion, and J. Y. Moyen. Quasi-interpretations a way to control resources. Theor. Comput. Sci., 412(25):2776–2796, June 2011.doi:10.1016/j.tcs.2011.02.007. 8Karl Crary. The Istari proof assistant.https://istarilogic.org/,

work page doi:10.1145/232627.232650 2011

[3] [3]

10 Ugo Dal Lago and Martin Hofmann

doi:10.1017/S0960129521000505. 10 Ugo Dal Lago and Martin Hofmann. Realizability models and implicit complexity.Theor. Comput. Sci., 412(20):2029–2047, April 2011.doi:10.1016/j.tcs.2010.12.025. 11 Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. Formal proof of polynomial-time complexity with quasi-interpretations. InProceedings o...

work page doi:10.1017/s0960129521000505 2029

[4] [4]

13 Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca

Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2007).doi:10.1016/j.entcs.2008.03.066. 13 Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. An Implicit Char- acterization of PSPACE.ACM Trans. Comput. Logic, 13(2):1–36, April

work page doi:10.1016/j.entcs.2008.03.066 2007

[5] [5]

14 Nathaniel Glover and Jan Hoffmann

doi: 10.1145/2159531.2159540. 14 Nathaniel Glover and Jan Hoffmann. LFPL: Revisited and Mechanized - Source Code of the Mechanization, May

work page doi:10.1145/2159531.2159540

[6] [6]

15 Sylvain Heraud and David Nowak

URL:https://doi.org/10.5281/zenodo.18348213. 15 Sylvain Heraud and David Nowak. A formalization of polytime functions. InProceedings of the Second International Conference on Interactive Theorem Proving, ITP ’11, page 119–134. Springer-Verlag, August

work page doi:10.5281/zenodo.18348213

[7] [7]

Two decades of automatic amortized resource analysis.Math

16 Jan Hoffmann and Steffen Jost. Two decades of automatic amortized resource analysis.Math. Struct. Comput. Sci., 32(6):729–759, March 2022.doi:10.1017/S0960129521000487. 17 Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS 1999, page...

work page doi:10.1017/s0960129521000487 2022

[8] [8]

Glover and J

N. Glover and J. Hoffmann 29 19 Martin Hofmann. The strength of non-size increasing computation. InProceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’02, page 260–269. Association for Computing Machinery, January 2002.doi:10.1145/503272.5 03297. 20 Martin Hofmann. Linear types and non-size-increasing polynom...

work page doi:10.1145/503272.5 2002

[9] [9]

24 Anton Lorenzen, Daan Leijen, and Wouter Swierstra

doi:10.1145/3779031.3779085. 24 Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP2: Fully in-Place Functional Program- ming.Proc. ACM Program. Lang., 7(ICFP):275–304, August 2023.doi:10.1145/3607840. 25 Jean-Yves Marion. Analysing the implicit complexity of programs.Inf. Comput., 183(1):2–18, May 2003.doi:10.1016/S0890-5401(03)00011-7. 26 Jean-Yves Ma...

work page doi:10.1145/3779031.3779085 2023

[10] [10]

Typable Fragments of Polynomial Automatic Amortized Resource Analysis

29 Long Pham and Jan Hoffmann. Typable Fragments of Polynomial Automatic Amortized Resource Analysis. In29th EACSL Annual Conference on Computer Science Logic, CSL 2021, volume 183 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 34:1– 34:19, Dagstuhl, Germany,

work page 2021

[11] [11]

30 Ramyaa Ramyaa and Daniel Leivant

Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi: 10.4230/LIPIcs.CSL.2021.34. 30 Ramyaa Ramyaa and Daniel Leivant. Ramified Corecurrence and Logspace.Electronic Notes in Theoretical Computer Science, 276:247–261, September

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

[12] [12]

31 Ulrich Schopp

Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 27.doi:10.1016/j.en tcs.2011.09.025. 31 Ulrich Schopp. Stratified Bounded Affine Logic for Logarithmic Space. InProceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS ’07, pages 411–420. IEEE Computer Society, July 2007.doi:10.1109/LICS.2007....

work page doi:10.1016/j.en 2011