An analysis of the Podelski-Rybalchenko termination theorem via bar recursion

DOI10.1093/LOGCOM/EXV058MaRDI QIDQ5225855zbMATH OpenOpenAlexFDO

Authors Stefano Berardi, Paulo Oliva, Silvia Steila

Publication date 29 July 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exv058

zbMATH Keywords

Ramsey's theoremtermination theoremintuitionismbar recursionwell-foundedness

Mathematics Subject Classification ID

Ramsey theory (05D10) Higher-type and set recursion theory (03D65) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Recommendations

• Reverse mathematical bounds for the termination theorem
• A proof-theoretic study of abstract termination principles
• An intuitionistic version of Ramsey's theorem and its use in program termination
• An intuitionistic analysis of size-change termination
• Ramsey theorem as an intuitionistic property of well founded relations

Cited in

(8)

• A direct proof of Schwichtenberg's bar recursion closure theorem
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
• scientific article; zbMATH DE number 7297814 (Why is no real title available?)
• Reverse mathematical bounds for the termination theorem
• An intuitionistic version of Ramsey's theorem and its use in program termination
• A combinatorial bound for a restricted form of the termination theorem
• Bar recursion is not computable via iteration

This page was built for publication: An analysis of the Podelski-Rybalchenko termination theorem via bar recursion

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