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

DOI10.1007/978-3-642-32347-8_17MaRDI QIDQ2914747zbMATHOpenAlexFDO

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)

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

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)