Termination of Isabelle Functions via Termination of Rewriting

DOI10.1007/978-3-642-22863-6_13zbMath1342.68289OpenAlexW1836046881MaRDI QIDQ3088004

Carsten Fuhs, René Thiemann, Christian Sternagel, Jürgen Giesl, Alexander Krauss

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Related Items (2)

Formal verification of termination criteria for first-order recursive functions ⋮ IsaFoR

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• CeTA
• Tyrolean
• AProVE
• LCF
• CoLoR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Matrix interpretations for proving termination of term rewriting
• Partial and nested recursive function definitions in higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Certification of Termination Proofs Using CeTA
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Certification of Automated Termination Proofs
• Certified Size-Change Termination
• Term Rewriting and All That
• CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES
• Verification of Erlang processes by dependency pairs
• Termination of logic programs: Transformational methods revisited

This page was built for publication: Termination of Isabelle Functions via Termination of Rewriting