Pages that link to "Item:Q4212925"

The following pages link to On the computational content of the axiom of choice (Q4212925):

Displaying 31 items.

• Realizability for Peano arithmetic with winning conditions in HON games (Q345704) (← links)
• The equivalence of bar recursion and open recursion (Q400424) (← links)
• The Peirce translation (Q408162) (← links)
• Bar recursion over finite partial functions (Q515562) (← links)
• Parameter-free polymorphic types (Q958481) (← links)
• Operational domain theory and topology of sequential programming languages (Q1013087) (← links)
• Uniform Heyting arithmetic (Q1772775) (← links)
• Dependent choice, `quote' and the clock (Q1884884) (← links)
• Limiting partial combinatory algebras (Q1884934) (← links)
• Minimum classical extensions of constructive theories (Q2117797) (← links)
• The effects of effects on constructivism (Q2133168) (← links)
• Programs from proofs using classical dependent choice (Q2482844) (← links)
• A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory (Q2683776) (← links)
• A Coalgebraic View of Bar Recursion and Bar Induction (Q2811334) (← links)
• Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
• A generalization of Nash's theorem with higher-order functionals (Q2831257) (← links)
• Sequential games and optimal strategies (Q3104817) (← links)
• Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs (Q3305635) (← links)
• Selection functions, bar recursion and backward induction (Q3559969) (← links)
• Realizability algebras III: some examples (Q4599612) (← links)
• Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
• THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT (Q4977221) (← links)
• (Q5129941) (← links)
• (Q5155683) (← links)
• Constructive forcing, CPS translations and witness extraction in Interactive realizability (Q5360214) (← links)
• Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 (Q5740401) (← links)
• Realizability interpretation of PA by iterated limiting PCA (Q5740403) (← links)
• Stateful Realizers for Nonstandard Analysis (Q6135755) (← links)
• Pumping, with or without choice (Q6536320) (← links)
• Zeta functions and the (linear) logic of Markov processes (Q6597969) (← links)
• A direct computational interpretation of second-order arithmetic via update recursion (Q6649499) (← links)