An abstract factorization theorem for explicit substitutions

DOI10.4230/LIPICS.RTA.2012.6zbMATH Open1437.68038MaRDI QIDQ5111891FDOQ5111891

Authors: Beniamino Accattoli 

Publication date: 27 May 2020

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

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)

Cited In (12)

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

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)