A semantics of evidence for classical arithmetic
From MaRDI portal
Publication:4836058
DOI10.2307/2275524zbMATH Open0829.03037OpenAlexW2071289523MaRDI QIDQ4836058FDOQ4836058
Authors: Thierry Coquand
Publication date: 21 January 1996
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2275524
Recommendations
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) First-order arithmetic and fragments (03F30)
Cited In (39)
- Fluctuations, effective learnability and metastability in analysis
- Herbrand's theorem as higher order recursion
- Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
- Games with 1-backtracking
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- Semirings of Evidence
- A sequent calculus for limit computable mathematics
- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Classical realizability and arithmetical formulæ
- Classical realizability in the CPS target language
- A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory
- Positive Arithmetic Without Exchange Is a Subclassical Logic
- Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves
- Dialogues and Proofs; Yankov’s Contribution to Proof Theory
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- A tale of additives and concurrency in game semantics
- A New Translation for Semi-classical Theories — Backtracking without CPS
- Game semantics of Martin-Löf type theory
- Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation
- Symmetry and Interactivity in Programming
- Program testing and the meaning explanations of intuitionistic type theory
- A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
- Mathematics based on incremental learning -- excluded middle and inductive inference
- Lorenzen and constructive mathematics
- Totality in arena games
- Sequential games and optimal strategies
- Programming interfaces and basic topology
- Realizability for Peano arithmetic with winning conditions in HON games
- Classical proof forestry
- Title not available (Why is that?)
- Toward the interpretation of non-constructive reasoning as non-monotonic learning
- Getting results from programs extracted from classical proofs
- Expansion trees with cut
- Propositional games with explicit strategies
- Between proof and truth
- Erratum to: ``Between proof and truth
- Imperative programs as proofs via game semantics
- Dependent choice, `quote' and the clock
This page was built for publication: A semantics of evidence for classical arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4836058)