The equivalence of bar recursion and open recursion
From MaRDI portal
Publication:400424
DOI10.1016/j.apal.2014.07.003zbMath1354.03058OpenAlexW2023101964MaRDI QIDQ400424
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
Related Items (7)
A universal algorithm for Krull's theorem ⋮ Higher-order games with dependent types ⋮ Well Quasi-orders and the Functional Interpretation ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Bar recursion over finite partial functions ⋮ Dependent choice as a termination principle ⋮ BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The Peirce translation
- Proving open properties by induction
- 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
- Programs from proofs using classical dependent choice
- On Spector's bar recursion
- Sequential games and optimal strategies
- 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
- On the computational content of the axiom of choice
- Constructive topology and combinatorics
- Strong normalisation for applied lambda calculi
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Modified bar recursion
This page was built for publication: The equivalence of bar recursion and open recursion
