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

DOI10.1016/j.apal.2015.08.002zbMath1378.03050OpenAlexW1138927884MaRDI QIDQ499082

Silvia Steila, Stefano Berardi

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

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

Related Items (5)

Reverse mathematical bounds for the termination theorem ⋮ A Combinatorial Bound for a Restricted Form of 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 ⋮ RAMSEY’S THEOREM FOR PAIRS ANDKCOLORS AS A SUB-CLASSICAL PRINCIPLE OF ARITHMETIC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Ramsey's theorem for pairs and provably recursive functions
• Constructing recursion operators in intuitionistic type theory
• Omega-termination is undecidable for totally terminating term rewriting systems
• Stop When You Are Almost-Full
• Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Ramsey Theorem as an Intuitionistic Property of Well Founded Relations
• The size-change principle for program termination
• An Intuitionistic Analysis of Size-change Termination
• Ramsey's theorem and recursion theory
• A constructive interpretation of Ramsey's theorem via the product of selection functions
• Static Analysis

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