Termination of algorithms over non-freely generated data types

DOI10.1007/3-540-61511-3_73zbMath1412.68261OpenAlexW1523188793MaRDI QIDQ4647505

Claus Sengler

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_73

zbMATH Keywords

inference ruleproof obligationtermination proofdata typeconstructor function

Mathematics Subject Classification ID

Related Items (2)

Termination of algorithms over non-freely generated data types ⋮ INKA: The next generation

Uses Software

• InKa
• CLAM
• Oyster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Proof by consistency
• Mechanizing structural induction. II: Strategies
• On proving the termination of algorithms by machine
• Algorithmic specifications: a constructive specification method for abstract data types
• Termination of algorithms over non-freely generated data types
• INKA: The next generation

This page was built for publication: Termination of algorithms over non-freely generated data types