Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
From MaRDI portal
(Redirected from Publication:2265415)
Cited in
(only showing first 100 items - show all)- Functorial polymorphism
- Some logical metatheorems with applications in functional analysis
- On quantitative convergence for stochastic processes: crossings, fluctuations and martingales
- Parameter-free polymorphic types
- A quantitative nonlinear strong ergodic theorem for Hilbert spaces
- Splittings and disjunctions in reverse mathematics
- A constructive analysis of learning in Peano arithmetic
- The finitary content of sunny nonexpansive retractions
- On Weihrauch reducibility and intuitionistic reverse mathematics
- Nonstandardness and the bounded functional interpretation
- Polymorphic extensions of simple type structures. With an application to a bar recursive minimization
- The equivalence of bar recursion and open recursion
- The Peirce translation
- Computations in fragments of intuitionistic propositional logic
- Nets and reverse mathematics
- Computability theory, nonstandard analysis, and their connections
- Constructive geometry and the parallel postulate
- Characterising Brouwer's continuity by bar recursion on moduli of continuity
- An application of proof mining to nonlinear iterations
- Pointwise hereditary majorization and some applications
- A note on equality in finite‐type arithmetic
- A(nother) characterization of intuitionistic propositional logic
- THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
- Strongly uniform bounds from semi-constructive proofs
- Types, abstraction, and parametric polymorphism, part 2
- Fragments of arithmetic
- The modified realizability topos
- Functional interpretations of feasibly constructive arithmetic
- Three faces of natural deduction
- On a weakening of Markov's Principle
- A logical aspect of parametric polymorphism
- Remarks on Herbrand normal forms and Herbrand realizations
- Total sets and objects in domain theory
- The lack of definable witnesses and provably recursive functions in intuitionistic set theories
- Functional Interpretations of Intuitionistic Linear Logic
- A proof-theoretic metatheorem for nonlinear semigroups generated by an accretive operator and applications
- Equivalents of the (weak) fan theorem
- An analysis of Tennenbaum's theorem in constructive type theory
- Using Ramsey's theorem once
- Herbrandized modified realizability
- \(\mathcal {BCDL}\): Basic constructive description logic
- Defining concurrent processes constructively
- On the uncountability of \(\mathbb{R}\)
- Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
- scientific article; zbMATH DE number 7269245 (Why is no real title available?)
- A simple proof of second-order strong normalization with permutative conversions
- On Goodman realizability
- A herbrandized functional interpretation of classical first-order logic
- Proof mining in \(L_{1}\)-approximation
- On computational properties of Cauchy problems generated by accretive operators
- Representations and the foundations of mathematics
- THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS)
- A semantic hierarchy for intuitionistic logic
- On the constructive and computational content of abstract mathematics
- Natural deduction for intuitionistic linear logic
- On maximal intermediate predicate constructive logics
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions
- Randomising realizability
- Splittings and robustness for the Heine-Borel theorem
- scientific article; zbMATH DE number 7447750 (Why is no real title available?)
- Decidable Kripke models of intuitionistic theories
- An arithmetic for polynomial-time computation
- A normal form for logical derivations implying one for arithmetic derivations
- Realizability interpretation of proofs in constructive analysis
- Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
- Equivalence of bar recursors in the theory of functionals of finite type
- A Computable Solution to Partee’s Temperature Puzzle
- A universal algorithm for Krull's theorem
- Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
- The biggest five of reverse mathematics
- On a second order propositional operator in intuitionistic logic
- On bounded functional interpretations
- Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
- Axiomatizing higher-order Kleene realizability
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- The strength of compactness in computability theory and nonstandard analysis
- Reverse mathematics and Weihrauch analysis motivated by finite complexity theory
- Well-foundedness in realizability
- Extensional models for polymorphism
- A functional interpretation for nonstandard arithmetic
- A complexity analysis of functional interpretations
- Modified realizability and predicate logic
- LCF considered as a programming language
- Completeness proofs for propositional logic with polynomial-time connectives
- The bounded functional interpretation of bar induction
- Constructing type systems over an operational semantics
- From constructivism to computer science
- A global representation of the recursive functions in the \(\lambda\)- calculus
- The basic feasible functionals in computable analysis
- The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
- Injecting uniformities into Peano arithmetic
- Computability in higher types, P and the completeness of type assignment
- Refining the arithmetical hierarchy of classical principles
- On uniform weak König's lemma
- Proof theory in the abstract
- Reverse mathematics and parameter-free transfer
- A propositional logic with explicit fixed points
- A version of the ∑1-reflection principle for CFA provable in PRA
- Bounded functional interpretation and feasible analysis
- Formalizing type operations using the ``image type constructor
This page was built for publication: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265415)
