Normalisation for higher-order calculi with explicit substitutions

DOI10.1016/j.tcs.2004.10.019zbMath1070.68055OpenAlexW2073527997MaRDI QIDQ1770414

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

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Combinatory reduction systems: Introduction and survey
• Descendants and origins in term rewriting.
• Perpetuality in a named lambda calculus with explicit substitutions
• A λ-calculus with explicit weakening and explicit substitution
• Strong normalization of substitutions
• Functional back-ends within the lambda-sigma calculus
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• Explicit substitutions
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Optimal normalization in orthogonal term rewriting systems

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