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

DOI10.1007/978-3-642-32347-8_17zbMATH Open1360.68768OpenAlexW16315125MaRDI QIDQ2914747FDOQ2914747

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

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

Mathematics Subject Classification ID

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

Cited In (8)

• Constructive decision via redundancy-free proof-search
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Certified Kruskal's tree theorem
• Ramsey's theorem for pairs and \(k\) colors as a sub-classical principle of arithmetic
• Variations on Noetherianness
• Reverse mathematical bounds for the termination theorem
• An intuitionistic version of Ramsey's theorem and its use in program termination
• 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)