Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs

DOI10.1007/978-3-030-20447-1_14zbMath1469.03161arXiv1812.05851OpenAlexW2903953552MaRDI QIDQ3305635

No author found.

Publication date: 10 August 2020

Published in: Mathesis Universalis, Computability and Proof (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1812.05851

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25)

Cites Work

• Fluctuations, effective learnability and metastability in analysis
• The equivalence of bar recursion and open recursion
• Bar recursion over finite partial functions
• Notions of computation and monads
• The epsilon calculus and Herbrand complexity
• Unifying functional interpretations
• Cut elimination for a simple formulation of epsilon calculus
• Ackermann's substitution method (remixed)
• Zur Widerspruchsfreiheit der Zahlentheorie
• Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
• Transfinite Update Procedures for Predicative Systems of Analysis
• Extracting Imperative Programs from Proofs: In-place Quicksort
• Existential witness extraction in classical realizability and via a negative translation
• Proofs and Computations
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• On the computational content of the axiom of choice
• Gödel's functional interpretation and the concept of learning
• A semantics of evidence for classical arithmetic
• On the No-Counterexample Interpretation
• Extracting verified decision procedures: DPLL and Resolution
• Logic for Gray-code Computation
• A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• A constructive interpretation of Ramsey's theorem via the product of selection functions
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs