Normalisation for higher-order calculi with explicit substitutions

DOI10.1016/J.TCS.2004.10.019MaRDI QIDQ1770414zbMATH OpenOpenAlexFDO

Authors Eduardo Bonelli

Publication date 6 April 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2004.10.019

zbMATH Keywords

Lambda calculusHigher-order rewritingExplicit substitutionsNeeded-strategiesNormalisation

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1956511
• The Theory of Calculi with Explicit Substitutions Revisited
• A Theory of Explicit Substitutions with Safe and Full Composition
• scientific article; zbMATH DE number 1342288
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones

Cites work

• scientific article; zbMATH DE number 1615230 (Why is no real title available?)
• scientific article; zbMATH DE number 1722698 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 599028 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1956511 (Why is no real title available?)
• scientific article; zbMATH DE number 794240 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A \(\lambda\)-calculus with explicit weakening and explicit substitution
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• Combinatory reduction systems: Introduction and survey
• Descendants and origins in term rewriting.
• Explicit substitutions
• Functional back-ends within the lambda-sigma calculus
• Optimal normalization in orthogonal term rewriting systems
• Perpetuality in a named lambda calculus with explicit substitutions
• Strong normalization of substitutions
• The lambda calculus. Its syntax and semantics. Rev. ed.
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(4)

• Combinatory reduction systems with explicit substitution that preserve strong normalisation
• scientific article; zbMATH DE number 1956511 (Why is no real title available?)
• scientific article; zbMATH DE number 2086241 (Why is no real title available?)
• The Theory of Calculi with Explicit Substitutions Revisited

This page was built for publication: Normalisation for higher-order calculi with explicit substitutions

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