The equivalence of bar recursion and open recursion

DOI10.1016/J.APAL.2014.07.003zbMATH Open1354.03058OpenAlexW2023101964MaRDI QIDQ400424FDOQ400424

Authors: Thomas Powell 

Publication date: 21 August 2014

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.2014.07.003

Recommendations

• On Spector's bar recursion
• Equivalence of bar recursors in the theory of functionals of finite type
• Modified bar recursion
• Bar recursion and products of selection functions
• Bar recursion over finite partial functions

zbMATH Keywords

bar recursionopen recursionprimitive recursive equivalenceGödel's system T

Mathematics Subject Classification ID

Higher-type and set recursion theory (03D65) Functionals in proof theory (03F10)

Cites Work

• Proving open properties by induction
• Constructive topology and combinatorics
• Title not available (Why is that?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Title not available (Why is that?)
• On the computational content of the axiom of choice
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Equivalence of bar recursors in the theory of functionals of finite type
• Programs from proofs using classical dependent choice
• Synthetic topology: of data types and classical spaces
• On Spector's bar recursion
• Sequential games and optimal strategies
• Title not available (Why is that?)
• Selection functions, bar recursion and backward induction
• Computational Interpretations of Analysis via Products of Selection Functions
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• Title not available (Why is that?)
• The Peirce translation
• Strong normalisation for applied lambda calculi
• Modified bar recursion
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (15)

• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Modified bar recursion
• Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
• Higher-order games with dependent types
• A universal algorithm for Krull's theorem
• Equivalence of bar recursors in the theory of functionals of finite type
• Bar recursion and products of selection functions
• System T and the product of selection functions
• Logical Approaches to Computational Barriers
• Title not available (Why is that?)
• Well quasi-orders and the functional interpretation
• Bar recursion is not computable via iteration
• Dependent choice as a termination principle
• Bar recursion over finite partial functions
• A direct proof of Schwichtenberg's bar recursion closure theorem

This page was built for publication: The equivalence of bar recursion and open recursion

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