Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
From MaRDI portal
Publication:2265415
Cited in
(only showing first 100 items - show all)- On the uncountability of \(\mathbb{R}\)
- On a second order propositional operator in intuitionistic logic
- Computable Kripke models and intermediate logics
- Projective sets, intuitionistically
- On the disjunctive Markov principle
- Constructing type systems over an operational semantics
- A logical uniform boundedness principle for abstract metric and hyperbolic spaces
- From Coinductive Proofs to Exact Real Arithmetic
- Parameter-free polymorphic types
- A higher-order calculus and theory abstraction
- An extension of the equivalence between Brouwer's fan theorem and weak König's lemma with a uniqueness hypothesis
- Remarks on Herbrand normal forms and Herbrand realizations
- On uniform weak König's lemma
- Proof theory in the abstract
- Proof mining and effective bounds in differential polynomial rings
- Choice and independence of premise rules in intuitionistic set theory
- The abstract type of the real numbers
- Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp
- Extended bar induction in applicative theories
- On a weakening of Markov's Principle
- The real-algebraic structure of Scott's model of intuitionistic analysis
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions
- Prenex normal form theorems in semi-classical arithmetic
- Solovay's relative consistency proof for FIM and BI
- Arithmetic complexity of the predicate logics of certain complete arithmetic theories
- Representations and the foundations of mathematics
- Realizability and intuitionistic logic
- A global representation of the recursive functions in the \(\lambda\)- calculus
- Nonstandardness and the bounded functional interpretation
- Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers)
- Primitive recursive selection functions for existential assertions over abstract algebras
- Well-foundedness in realizability
- Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction
- A proof-theoretic investigation of a logic of positions
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Completeness proofs for propositional logic with polynomial-time connectives
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- The basic feasible functionals in computable analysis
- König's lemma, weak König's lemma, and the decidable fan theorem
- Injecting uniformities into Peano arithmetic
- A functional interpretation for nonstandard arithmetic
- The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
- On the constructive and computational content of abstract mathematics
- Computations in fragments of intuitionistic propositional logic
- \(\mathcal {BCDL}\): Basic constructive description logic
- Some derived rules of intuitionistic second order arithmetic
- Intuitionist type theory and the free topos
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Markov's rule revisited
- Realizability interpretation of proofs in constructive analysis
- A semantic hierarchy for intuitionistic logic
- Intuitionistic fixed point logic
- Some principles weaker than Markov's principle
- The admissible rules of \(\mathsf{BD}_2\) and \(\mathsf{GSc}\)
- A complexity analysis of functional interpretations
- Total sets and objects in domain theory
- Functional interpretation of Aczel's constructive set theory
- Functional interpretations of linear and intuitionistic logic
- On the syntax of Martin-Löf's type theories
- A constructive version of Tarski's geometry
- A propositional logic with explicit fixed points
- Computability in higher types, P\(\omega\) and the completeness of type assignment
- Logical metatheorems for abstract spaces axiomatized in positive bounded logic
- The bounded functional interpretation of bar induction
- From constructivism to computer science
- Axiomatizing higher-order Kleene realizability
- Constructive geometry and the parallel postulate
- On bounded functional interpretations
- Term extraction and Ramsey's theorem for pairs
- Set existence property for intuitionistic theories with dependent choice
- Strongly uniform bounds from semi-constructive proofs
- Extraction and verification of programs by analysis of formal proofs
- CZF and second order arithmetic
- Dialectica interpretation with fine computational control
- Equivalence of bar recursors in the theory of functionals of finite type
- On specifications, subset types and interpretation of proposition in type theory
- Bounded functional interpretation and feasible analysis
- The lack of definable witnesses and provably recursive functions in intuitionistic set theories
- A quantitative nonlinear strong ergodic theorem for Hilbert spaces
- Some logical metatheorems with applications in functional analysis
- Pointwise hereditary majorization and some applications
- Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)
- An arithmetic for polynomial-time computation
- Uniform Heyting arithmetic
- Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
- A constructive approach to nonstandard analysis
- The equivalence of bar recursion and open recursion
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
- Intuitionistic mereology
- Program extraction for 2-random reals
- The semantics of second-order lambda calculus
- LCF considered as a programming language
- Negative translations not intuitionistically equivalent to the usual ones
- Innovations in computational type theory using Nuprl
- Recursion over realizability structures
- Some results on cut-elimination, provable well-orderings, induction and reflection
- The Peirce translation
- Uniform proofs as a foundation for logic programming
- Program extraction from normalization proofs
- A(nother) characterization of intuitionistic propositional logic
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)
