Constructive forcing, CPS translations and witness extraction in Interactive realizability
From MaRDI portal
Publication:5360214
DOI10.1017/S0960129515000468zbMath1456.03109OpenAlexW2219039436MaRDI QIDQ5360214
Publication date: 28 September 2017
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129515000468
Other constructive mathematics (03F65) Second- and higher-order arithmetic and fragments (03F35) Other aspects of forcing and Boolean-valued models (03E40)
Related Items (2)
Stateful Realizers for Nonstandard Analysis ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Continuity of Gödel's system T definable functionals via effectful forcing
- A constructive analysis of learning in Peano arithmetic
- Notions of computation and monads
- Lectures on the Curry-Howard isomorphism
- Epsilon substitution method for elementary analysis
- Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
- Transfinite Update Procedures for Predicative Systems of Analysis
- Realizability algebras: a program to well order R
- A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
- Selection functions, bar recursion and backward induction
- Relativized realizability in intuitionistic arithmetic of all finite types
- On the computational content of the axiom of choice
- Forcing in Proof Theory
- Eliminating definitions and Skolem functions in first-order logic
- Strong normalisation for applied lambda calculi
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1
- On the Interpretation of Non-Finitist Proofs--Part I
This page was built for publication: Constructive forcing, CPS translations and witness extraction in Interactive realizability
