Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
A semantics of evidence for classical arithmetic - MaRDI portal

A semantics of evidence for classical arithmetic

From MaRDI portal
Publication:4836058

DOI10.2307/2275524zbMath0829.03037OpenAlexW2071289523MaRDI QIDQ4836058

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




Related Items (35)

On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theoremDialogues and Proofs; Yankov’s Contribution to Proof TheoryGetting results from programs extracted from classical proofsDependent choice, `quote' and the clockRealizability for Peano arithmetic with winning conditions in HON gamesBetween proof and truthErratum to: ``Between proof and truthImperative programs as proofs via game semanticsFluctuations, effective learnability and metastability in analysisPositive Arithmetic Without Exchange Is a Subclassical LogicA finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theoryClassical realizability and arithmetical formulæGame semantics of Martin-Löf type theoryTotality in arena gamesGames with 1-backtrackingClassical proof forestryA Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful ProgramsClassical realizability in the CPS target languageHerbrand's theorem as higher order recursionSymmetry and Interactivity in ProgrammingA sequent calculus for limit computable mathematicsInteractive Realizability for second-order Heyting arithmetic with EM1 and SK1Unnamed ItemToward the interpretation of non-constructive reasoning as non-monotonic learningGödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample InterpretationA New Translation for Semi-classical Theories — Backtracking without CPSInteractive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTIONSequential games and optimal strategiesExpansion trees with cutProgram Testing and the Meaning Explanations of Intuitionistic Type TheoryProgramming interfaces and basic topologyLorenzen and Constructive MathematicsMathematics based on incremental learning -- excluded middle and inductive inference




This page was built for publication: A semantics of evidence for classical arithmetic