Dependent choice, `quote' and the clock

DOI10.1016/S0304-3975(02)00776-4zbMath1169.03328OpenAlexW1971613396MaRDI QIDQ1884884

Jean-Louis Krivine

Publication date: 27 October 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(02)00776-4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Axiom of choice and related propositions (03E25) Combinatory logic and lambda calculus (03B40)

Related Items (25)

Getting results from programs extracted from classical proofs ⋮ Realizability for Peano arithmetic with winning conditions in HON games ⋮ Between proof and truth ⋮ Erratum to: ``Between proof and truth ⋮ A realizability interpretation of Church's simple theory of types ⋮ The category of implicative algebras and realizability ⋮ Realizability algebras III: some examples ⋮ Classical realizability and arithmetical formulæ ⋮ Totality in arena games ⋮ Specifying Peirce's law in classical realizability ⋮ Ordered combinatory algebras and realizability ⋮ Realizability in ordered combinatory algebras with adjunction ⋮ Intuitionistic fixed point logic ⋮ A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract) ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Verificationism and Classical Realizability ⋮ A call-by-name lambda-calculus machine ⋮ A Survey of Classical Realizability ⋮ Krivine's classical realisability from a categorical perspective ⋮ Proofs, programs, processes ⋮ Programs from proofs using classical dependent choice ⋮ Relating Classical Realizability and Negative Translation for Existential Witness Extraction ⋮ Syntax vs. semantics: A polarized approach ⋮ On the necessity of some topological spaces

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof theory. 2nd ed
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Mathematical significance of consistency proofs
• On the computational content of the axiom of choice
• A semantics of evidence for classical arithmetic
• On the No-Counterexample Interpretation
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

This page was built for publication: Dependent choice, `quote' and the clock