An abstract factorization theorem for explicit substitutions

DOI10.4230/LIPICS.RTA.2012.6MaRDI QIDQ5111891zbMATH OpenFDO

Authors Beniamino Accattoli

Publication date 27 May 2020

zbMATH Keywords

standardization\(\lambda\)-calculusdiagrammatic reasoningexplicit substitutionsabstract rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• A nonstandard standardization theorem
• A Theory of Explicit Substitutions with Safe and Full Composition
• The Theory of Calculi with Explicit Substitutions Revisited
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Explicit substitution. On the edge of strong normalization

Cited in

(13)

• A Fresh Look at the λ-Calculus
• Decomposition theorem on invertible substitutions
• A faithful and quantitative notion of distant reduction for generalized applications
• On the value of variables
• Tight typings and split bounds, fully developed
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Proof nets and the call-by-value \(\lambda\)-calculus
• Factorization and normalization, essentially
• A nonstandard standardization theorem
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• The Negligible and Yet Subtle Cost of Pattern Matching
• Factorization in call-by-name and call-by-value calculi via linear logic

This page was built for publication: An abstract factorization theorem for explicit substitutions

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