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

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) General topics in the theory of algorithms (68W01)

Related Items

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