On the invariance of the unitary cost model for head reduction

DOI10.4230/LIPICS.RTA.2012.22zbMATH Open1437.68039arXiv1202.1641MaRDI QIDQ5111892FDOQ5111892

Authors: Beniamino Accattoli, Ugo Dal Lago 

Publication date: 27 May 2020

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

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

zbMATH Keywords

implicit computational complexitylambda calculuscost modelsexplicit substitutions

Mathematics Subject Classification ID

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

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
• Logical Approaches to Computational Barriers
• Tight typings and split bounds, fully developed
• (Leftmost-outermost) beta reduction is invariant, indeed
• (In)efficiency and reasonable cost models
• 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
• Linear additives
• On the value of variables
• 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)