An insertion operator preserving infinite reduction sequences

DOI10.1017/S0960129508006816MaRDI QIDQ3520149zbMATHFDO

Authors David Chemouil

Publication date 15 August 2008

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

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)

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

Cites work

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

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)