(Leftmost-Outermost) Beta Reduction is Invariant, Indeed

DOI10.2168/LMCS-12(1:4)2016zbMath1394.68137arXiv1601.01233MaRDI QIDQ2794671

Beniamino Accattoli, Ugo Dal Lago

Publication date: 11 March 2016

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

invarianceoperational semanticslinear logiclambda calculussharingstandardizationcost models

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items (19)

The Negligible and Yet Subtle Cost of Pattern Matching ⋮ On the enumeration of closures and environments with an application to random generation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Tight typings and split bounds, fully developed ⋮ Focused linear logic and the \(\lambda\)-calculus ⋮ Unnamed Item ⋮ Factorization and normalization, essentially ⋮ Classical By-Need ⋮ Unnamed Item ⋮ Reasonable space for the \(\lambda \)-calculus, logarithmically ⋮ Exponentials as substitutions and the cost of cut elimination in linear logic ⋮ The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus ⋮ A Fresh Look at the λ-Calculus ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Is the Optimal Implementation Inefficient? Elementarily Not ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs ⋮ (In)efficiency and reasonable cost models

This page was built for publication: (Leftmost-Outermost) Beta Reduction is Invariant, Indeed