Classical realizability and arithmetical formulæ
From MaRDI portal
Publication:5360216
DOI10.1017/S0960129515000559zbMath1456.03026arXiv1403.0875OpenAlexW2963002228MaRDI QIDQ5360216
Mauricio German Guillermo, Étienne Miquey
Publication date: 28 September 2017
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1403.0875
Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Cites Work
- Combinatory logic. With two sections by William Craig.
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Dependent choice, `quote' and the clock
- A symmetric lambda calculus for classical program extraction
- A call-by-name lambda-calculus machine
- Realizability algebras II : new models of ZF + DC
- The duality of computation
- Specifying Peirce's law in classical realizability
- Existential witness extraction in classical realizability and via a negative translation
- Realizability algebras: a program to well order R
- Classical Program Extraction in the Calculus of Constructions
- Proofs of strong normalisation for second order classical natural deduction
- A semantics of evidence for classical arithmetic
- On the structure of classical realizability models of ZF
- On the Interpretation of Non-Finitist Proofs--Part I
- On the interpretation of non-finitist proofs–Part II
- On the interpretation of intuitionistic number theory
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
