An intuitionistic version of Ramsey's theorem and its use in program termination

DOI10.1016/J.APAL.2015.08.002MaRDI QIDQ499082zbMATH OpenOpenAlexFDO

Authors Stefano Berardi, Silvia Steila

Publication date 29 September 2015

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2015.08.002

zbMATH Keywords

Ramsey's theoremintuitionisminductive definitionstermination of while-programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Ramsey theory (05D10) Intuitionistic mathematics (03F55)

Recommendations

• Ramsey theorem as an intuitionistic property of well founded relations
• An intuitionistic analysis of size-change termination
• scientific article; zbMATH DE number 517049
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• Another proof of the intuitionistic Ramsey theorem

Cites work

• scientific article; zbMATH DE number 4134034 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 512769 (Why is no real title available?)
• scientific article; zbMATH DE number 3310901 (Why is no real title available?)
• scientific article; zbMATH DE number 3365217 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• A constructive interpretation of Ramsey's theorem via the product of selection functions
• An intuitionistic analysis of size-change termination
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Constructing recursion operators in intuitionistic type theory
• Omega-termination is undecidable for totally terminating term rewriting systems
• Ramsey theorem as an intuitionistic property of well founded relations
• Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Ramsey's theorem and recursion theory
• Ramsey's theorem for pairs and provably recursive functions
• Static Analysis
• Stop when you are almost-full. Adventures in constructive termination
• The size-change principle for program termination
• Transition invariants and transition predicate abstraction for program termination

Cited in

(10)

• Another proof of the intuitionistic Ramsey theorem
• Ramsey theorem as an intuitionistic property of well founded relations
• An intuitionistic analysis of size-change termination
• Ramsey's theorem for pairs and \(k\) colors as a sub-classical principle of arithmetic
• Reverse mathematical bounds for the termination theorem
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• A combinatorial bound for a restricted form of the termination theorem
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• scientific article; zbMATH DE number 517049 (Why is no real title available?)

This page was built for publication: An intuitionistic version of Ramsey's theorem and its use in program termination

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