Reasonable Space for the λ-Calculus, Logarithmically
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Abstract
Can the λ-calculus be considered a reasonable computational model? Can we use it for measuring the time and space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the λ-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to accommodate logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value λ-calculus.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 8c68a2c1-3f67-4608-9436-f236c95dd199Cited by top-tier papers2
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear LogicBeniamino AccattoliLICS 2022 · 5 citations
- A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-CalculusThibaut BalabonskiLICS 2026 · 1 citation
Builds on4
- Strong Call-by-Value is Reasonable, ImplosivelyBeniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti CoenLICS 2021 · 21 citations
- The (In)Efficiency of interactionBeniamino Accattoli, Ugo Dal Lago, Gabriele VanoniPOPL 2021 · 13 citations
- The Space of InteractionBeniamino Accattoli, Ugo Dal Lago, Gabriele VanoniLICS 2021 · 4 citations
- The weak call-by-value λ-calculus is reasonable for both time and spaceYannick Forster, Fabian Kunze, Marc RothPOPL 2020 · 1 citation
Related papers
- A Compositional Cost Model for the λ-calculusJames LairdLICS 2021
- Simulating Time with Square-Root SpaceR. Ryan WilliamsSTOC 2025 · 1 citation
- Resource-Aware Soundness for Big-Step SemanticsRiccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena ZuccaOOPSLA 2023 · 6 citations
- Recurrence extraction for functional programs through call-by-push-valueG. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman DannerPOPL 2020 · 20 citations
- A unifying type-theory for higher-order (amortized) cost analysisVineet Rajani, Marco Gaboardi, Deepak Garg, Jan HoffmannPOPL 2021 · 26 citations
