scientific article; zbMATH DE number 7471663
From MaRDI portal
Publication date: 9 February 2022
Full work available at URL: https://arxiv.org/abs/1212.0020
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
quantified modal logicautomatic program synthesiscode-carrying classical proofsextractive Proof TheoryKreisel implicationProof Mining
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Light Dialectica revisited
- Unifying functional interpretations
- Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings
- A game semantics for linear logic
- Dialectica categories for the Lambek calculus
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Getting results from programs extracted from classical proofs
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- An application of proof mining to nonlinear iterations
- Full classical S5 in natural deduction with weak normalization
- Tableau methods of proof for modal logics
- Extensional Gödel functional interpretation. A consistency proof of classical analysis
- A parametrised functional interpretation of Heyting arithmetic
- A judgmental reconstruction of modal logic
- Light Dialectica Program Extraction from a Classical Fibonacci Proof
- Hybrid Functional Interpretations of Linear and Intuitionistic Logic
- Exploring the Computational Content of the Infinite Pigeonhole Principle
- Proofs and Computations
- Proof Analysis
- Light monotone Dialectica methods for proof mining
- Hybrid Functional Interpretations
- Extraction in Coq: An Overview
- Dialectica Interpretation with Fine Computational Control
- Nonexpansive iterations in uniformly convex $W$-hyperbolic spaces
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- On Tao's “finitary” infinite pigeonhole principle
- Unifying Functional Interpretations: Past and Future
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Logical Approaches to Computational Barriers
- A note on Spector's quantifier-free rule of extensionality
- Refined program extraction from classical proofs
