Generalized and formalized uncurrying

DOI10.1007/978-3-642-24364-6_17zbMATH Open1348.68086OpenAlexW1849654074MaRDI QIDQ3172898FDOQ3172898

René Thiemann, Christian Sternagel

Publication date: 7 October 2011

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24364-6_17

Recommendations

• Uncurrying for Termination
• Uncurrying for termination and complexity
• Comparing curried and uncurried rewriting
• Higher-order unCurrying
• Confluence of curried term-rewriting systems

zbMATH Keywords

term rewritinginteractive theorem provingterminationdependency pairsuncurryingformalization

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Certification of Termination Proofs Using CeTA
• Isabelle/HOL. A proof assistant for higher-order logic
• Term Rewriting and All That
• Comparing curried and uncurried rewriting
• Signature extensions preserve termination. An alternative proof via dependency pairs
• Frontiers of Combining Systems
• Uncurrying for Termination
• Mechanizing and improving dependency pairs

Cited In (4)

• Comparing curried and uncurried rewriting
• Higher-order unCurrying
• Uncurrying for termination and complexity
• A Lambda-Free Higher-Order Recursive Path Order

Uses Software

• Isabelle/HOL
• CeTA
• Tyrolean
• AProVE
• CoLoR
• Jambox
• A3PAT

This page was built for publication: Generalized and formalized uncurrying

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