Generalized and formalized uncurrying

DOI10.1007/978-3-642-24364-6_17MaRDI QIDQ3172898zbMATH OpenOpenAlexFDO

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

dependency pairsformalizationinteractive theorem provingterm rewritingterminationuncurrying

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

(8)

• Comparing curried and uncurried rewriting
• A Lambda-Free Higher-Order Recursive Path Order
• Uncurrying for termination and complexity
• Uncurrying for Termination
• Higher-order unCurrying
• Certifying the weighted path order (invited talk)
• An applicative multiset path order
• A verified framework for higher-order uncurrying optimizations

Describes a project that uses

Uses Software

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

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)