An insertion operator preserving infinite reduction sequences

DOI10.1017/S0960129508006816zbMATH Open1153.68025MaRDI QIDQ3520149FDOQ3520149

Authors: David Chemouil 

Publication date: 15 August 2008

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Recommendations

• TERMINATION OF ABSTRACT REDUCTION SYSTEMS
• Termination of combined (rewrite and λ-calculus) systems
• Non-standard reductions and categorical models in typed lambda-calculus
• Adding algebraic rewriting to the untyped lambda calculus
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS

zbMATH Keywords

reduction systems

Mathematics Subject Classification ID

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

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Term Rewriting and All That
• On the union of well-founded relations
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Isomorphisms of simple inductive types through extensional rewriting

This page was built for publication: An insertion operator preserving infinite reduction sequences

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