Generalized and formalized uncurrying

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

Authors Christian Sternagel, René Thiemann

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

zbMATH Keywords

term rewritinginteractive theorem provingterminationdependency pairsuncurryingformalization

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

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

Cites work

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

Cited in

(6)

• Higher-order unCurrying
• A Lambda-Free Higher-Order Recursive Path Order
• Uncurrying for Termination
• A verified framework for higher-order uncurrying optimizations
• Uncurrying for termination and complexity
• Comparing curried and uncurried rewriting

Describes a project that uses

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)