Enhancing dependency pair method using strong computability in simply-typed term rewriting

DOI10.1007/S00200-007-0046-9MaRDI QIDQ2460908zbMATH OpenOpenAlexFDO

Authors Keiichirou Kusakari, Masahiko Sakai

Publication date 19 November 2007

Published in Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00200-007-0046-9

zbMATH Keywords

dependency pairplain function-passingsimply-typed term rewriting systemstrong computabilitytermination

Mathematics Subject Classification ID

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

Recommendations

• Term Rewriting and Applications
• Argument filterings and usable rules for simply typed dependency pairs
• Dependency Pairs for Rewriting with Non-free Constructors
• Refinement types as higher-order dependency pairs
• scientific article; zbMATH DE number 2043542

Cites work

• Affine-based size-change termination.
• Automated Reasoning
• Comparing curried and uncurried rewriting
• Definitional interpreters for higher-order programming languages
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 1615229 (Why is no real title available?)
• scientific article; zbMATH DE number 1722711 (Why is no real title available?)
• scientific article; zbMATH DE number 578226 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• scientific article; zbMATH DE number 1765702 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• Improving dependency pairs
• Intensional interpretations of functionals of finite type I
• Logic for Programming, Artificial Intelligence, and Reasoning
• Modular and incremental automated termination proofs
• Modular and incremental proofs of AC-termination
• Modular termination proofs for rewriting using dependency pairs
• Orderings for term-rewriting systems
• Rewriting Techniques and Applications
• Rewriting Techniques and Applications
• Term Rewriting and Applications
• Termination of term rewriting using dependency pairs
• The size-change principle and dependency pairs for termination of term rewriting
• The size-change principle for program termination

Cited in

(8)

• Normal higher-order termination
• Harnessing first order termination provers using higher order dependency pairs
• Uncurrying for termination and complexity
• Argument filterings and usable rules for simply typed dependency pairs
• Size-based termination of higher-order rewriting
• Dependency pairs termination in dependent type theory modulo rewriting
• Term Rewriting and Applications
• Higher-order constrained dependency pairs for (universal) computability

Describes a project that uses

Uses Software

• ML
• AProVE

This page was built for publication: Enhancing dependency pair method using strong computability in simply-typed term rewriting

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