Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)

DOI10.4230/LIPICS.FSCD.2022.1MaRDI QIDQ6544095zbMATH OpenFDO

Authors Cynthia Kop

Publication date 27 May 2024

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2022.1

zbMATH Keywords

algebra interpretationsdependency pairshigher-order term rewritingmodularitytermination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• A recursive path ordering for higher-order terms in η-long β-normal form
• Harnessing first order termination provers using higher order dependency pairs
• scientific article; zbMATH DE number 1765695
• Normal higher-order termination

Cited in

(1)

• Higher-order constrained dependency pairs for (universal) computability

This page was built for publication: Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)

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