The following pages link to (Q3882452):
Displaying 50 items.
- Interpretation of constructive multi-typed theory in the theory of arithmetical truth (Q266212) (← links)
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP (Q476116) (← links)
- Explicit mathematics: power types and overloading (Q556826) (← links)
- Admissible closures of polynomial time computable arithmetic (Q634777) (← links)
- The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories (Q639666) (← links)
- The provably terminating operations of the subsystem PETJ of explicit mathematics (Q639690) (← links)
- A proof-theoretic characterization of the basic feasible functionals (Q706620) (← links)
- Extended bar induction in applicative theories (Q753810) (← links)
- Intensionality in mathematics (Q762052) (← links)
- Realizability and intuitionistic logic (Q792319) (← links)
- Generalizing classical and effective model theory in theories of operations and classes (Q810008) (← links)
- Proof-theoretical analysis: Weak systems of functions and classes (Q911585) (← links)
- Proofs and programs: A naïve approach to program extraction (Q912594) (← links)
- Primitive recursive selection functions for existential assertions over abstract algebras (Q941429) (← links)
- Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp (Q1050769) (← links)
- Monotone inductive definitions in a constructive theory of functions and classes (Q1115865) (← links)
- A theory for program and data type specification (Q1199933) (← links)
- Constructive mathematics: a foundation for computable analysis (Q1292399) (← links)
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I (Q1314542) (← links)
- Realizability interpretation of generalized inductive definitions (Q1331920) (← links)
- The strength of some Martin-Löf type theories (Q1344548) (← links)
- Formalizing non-termination of recursive programs (Q1349246) (← links)
- On the proof-theoretic strength of monotone induction in explicit mathematics (Q1356976) (← links)
- A first order logic of effects (Q1390955) (← links)
- Theories with self-application and computational complexity. (Q1427856) (← links)
- The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule (Q1577487) (← links)
- Arithmetical conservation results (Q1688961) (← links)
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice (Q1756495) (← links)
- Towards a computation system based on set theory (Q1825191) (← links)
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe (Q1861330) (← links)
- Universes over Frege structures (Q1861539) (← links)
- Totality in applicative theories (Q1896484) (← links)
- Understanding uniformity in Feferman's explicit mathematics (Q1899146) (← links)
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. II (Q1919537) (← links)
- Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels (Q1923579) (← links)
- Truth and the philosophy of mathematics (Q2080591) (← links)
- Intuitionistic fixed point logic (Q2220485) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) (Q2232317) (← links)
- What is constructive mathematics? (Q2266012) (← links)
- A flexible type system for the small Veblen ordinal (Q2312096) (← links)
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) (Q2344720) (← links)
- Metamathematical properties of a constructive multi-typed theory (Q2363505) (← links)
- Systems of explicit mathematics with non-constructive \(\mu\)-operator and join (Q2563984) (← links)
- Remarks on applicative theories (Q2566067) (← links)
- Reflections on reflections in explicit mathematics (Q2566068) (← links)
- Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory (Q2566070) (← links)
- On the collection of points of a formal space (Q2575767) (← links)
- A feasible theory of truth over combinatory algebra (Q2637706) (← links)
- Extending constructive operational set theory by impredicative principles (Q3008060) (← links)
- About Truth and Types (Q3305551) (← links)