Stop when you are almost-full. Adventures in constructive termination

DOI10.1007/978-3-642-32347-8_17MaRDI QIDQ2914747zbMATH OpenOpenAlexFDO

Authors Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt

Publication date 20 September 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_17

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• An intuitionistic analysis of size-change termination
• The size-change principle for program termination
• Size-change termination and transition invariants
• A proof-theoretic study of abstract termination principles
• Ramsey versus lexicographic termination proving

Cited in

(8)

• Certified Kruskal's tree theorem
• Reverse mathematical bounds for the termination theorem
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Ramsey's theorem for pairs and \(k\) colors as a sub-classical principle of arithmetic
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Variations on Noetherianness
• Constructive decision via redundancy-free proof-search
• Admissible ordering on monomials is well-founded: a constructive proof

This page was built for publication: Stop when you are almost-full. Adventures in constructive termination

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