The equivalence of bar recursion and open recursion

DOI10.1016/J.APAL.2014.07.003MaRDI QIDQ400424zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(15)

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

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)