On the invariance of the unitary cost model for head reduction

DOI10.4230/LIPICS.RTA.2012.22MaRDI QIDQ5111892zbMATH OpenFDO

Authors Beniamino Accattoli, Ugo Dal Lago

Publication date 27 May 2020

Full work available at URL https://arxiv.org/abs/1202.1641

zbMATH Keywords

cost modelsexplicit substitutionsimplicit computational complexitylambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Logical Approaches to Computational Barriers
• Beta reduction is invariant, indeed
• (Leftmost-outermost) beta reduction is invariant, indeed
• The weak lambda calculus as a reasonable machine
• (In)efficiency and reasonable cost models

Cited in

(19)

• On sharing, memoization, and polynomial time
• Processes against tests: on defining contextual equivalences
• Call-by-value lambda calculus as a model of computation in Coq
• (In)efficiency and reasonable cost models
• On the value of variables
• (Leftmost-outermost) beta reduction is invariant, indeed
• Beta reduction is invariant, indeed
• A Fresh Look at the λ-Calculus
• Tight typings and split bounds, fully developed
• Logical Approaches to Computational Barriers
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Reasonable space for the -calculus, logarithmically
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Processes, systems \& tests: defining contextual equivalences
• Linear additives
• IMELL cut elimination with linear overhead
• Call-by-value and call-by-name: a simple proof of a classic theorem
• Reasonable space for the -calculus, logarithmically
• Barendregt's theory of the -calculus, refreshed and formalized

This page was built for publication: On the invariance of the unitary cost model for head reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111892)