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

implicit computational complexitylambda calculuscost modelsexplicit substitutions

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

(15)

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

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)