Combinatory reduction systems with explicit substitution that preserve strong normalisation

DOI10.1007/3-540-61464-8_51MaRDI QIDQ5055859zbMATH OpenOpenAlexFDO

Authors Roel Bloo, Kristoffer H. Rose

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_51

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 1070568
• scientific article; zbMATH DE number 1342288
• Explicit substitution. On the edge of strong normalization
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Normalisation for higher-order calculi with explicit substitutions

Cites work

• Combinatory reduction systems: Introduction and survey
• Explicit cyclic substitutions
• Explicit substitutions
• scientific article; zbMATH DE number 2185670 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 1130260 (Why is no real title available?)
• scientific article; zbMATH DE number 1499112 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The Mechanical Evaluation of Expressions

Cited in

(5)

• Explicit substitution. On the edge of strong normalization
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Pattern matching as cut elimination
• scientific article; zbMATH DE number 1015107 (Why is no real title available?)

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Combinatory reduction systems with explicit substitution that preserve strong normalisation

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