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

DOI10.1016/J.APAL.2015.08.002zbMATH Open1378.03050OpenAlexW1138927884MaRDI QIDQ499082FDOQ499082

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

Recommendations

• Ramsey theorem as an intuitionistic property of well founded relations
• An intuitionistic analysis of size-change termination
• [[:Publication:4282577|Title not available (Why is that?)]]
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• Another proof of the intuitionistic Ramsey theorem

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• The size-change principle for program termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Ramsey's theorem and recursion theory
• Static Analysis
• Constructing recursion operators in intuitionistic type theory
• Omega-termination is undecidable for totally terminating term rewriting systems
• Title not available (Why is that?)
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Ramsey Theorem as an Intuitionistic Property of Well Founded Relations
• An Intuitionistic Analysis of Size-change Termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• A constructive interpretation of Ramsey's theorem via the product of selection functions
• Ramsey's theorem for pairs and provably recursive functions

Cited In (7)

• Another proof of the intuitionistic Ramsey theorem
• A Combinatorial Bound for a Restricted Form of the Termination Theorem
• 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
• RAMSEY’S THEOREM FOR PAIRS ANDKCOLORS AS A SUB-CLASSICAL PRINCIPLE OF ARITHMETIC
• Title not available (Why is that?)

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)