Validating Brouwer's continuity principle for numbers using named exceptions
From MaRDI portal
Recommendations
- Gentzen's consistency proofs for arithmetic
- Justification of the continuum hypothesis
- Real Number Calculations and Theorem Proving
- Logic of Proofs for Bounded Arithmetic
- scientific article; zbMATH DE number 4006264
- Discontinuities of provably correct operators on the provably recursive real numbers
- Semantical proofs of correctness for programs performing non-deterministic tests on real numbers
- scientific article; zbMATH DE number 3255033
Cites work
- scientific article; zbMATH DE number 1612495 (Why is no real title available?)
- scientific article; zbMATH DE number 1722663 (Why is no real title available?)
- scientific article; zbMATH DE number 2185662 (Why is no real title available?)
- scientific article; zbMATH DE number 4180818 (Why is no real title available?)
- scientific article; zbMATH DE number 3850461 (Why is no real title available?)
- scientific article; zbMATH DE number 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 4002093 (Why is no real title available?)
- scientific article; zbMATH DE number 4068858 (Why is no real title available?)
- scientific article; zbMATH DE number 4070894 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 3557754 (Why is no real title available?)
- scientific article; zbMATH DE number 3573834 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 482822 (Why is no real title available?)
- scientific article; zbMATH DE number 1113859 (Why is no real title available?)
- scientific article; zbMATH DE number 1538034 (Why is no real title available?)
- scientific article; zbMATH DE number 1795233 (Why is no real title available?)
- scientific article; zbMATH DE number 1841844 (Why is no real title available?)
- scientific article; zbMATH DE number 3216177 (Why is no real title available?)
- scientific article; zbMATH DE number 2242589 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A System F with Call-by-Name Exceptions
- A computational interpretation of forcing in type theory
- A constructive logic behind the catch and throw mechanism
- A constructive model of uniform continuity
- A dependent nominal type theory
- A dependent type theory with abstractable names
- A fresh look at programming with names and binders
- A note on Bar Induction in Constructive Set Theory
- A note on forcing and type theory
- A simple nominal type theory
- A type system for call-by-name exceptions
- An intuitionistic λ-calculus with exceptions
- Arguments for the Continuity Principle
- Bar induction. The good, the bad, and the ugly
- Bar recursion and products of selection functions
- Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
- Computational foundations of basic recursive function theory
- Computer Science Logic
- Computing with Functionals—Computability Theory or Computer Science?
- Constructive set theory and Brouwerian principles
- Constructivism in mathematics. An introduction. Volume II
- Continuity of Gödel's system T definable functionals via effectful forcing
- Dependent types for nominal terms with atom substitutions
- Edinburgh LCF. A mechanized logic of computation
- Exhaustible sets in higher-type computation
- Forcing in Proof Theory
- Formal program optimization in Nuprl using computational equivalence and partial types
- Formalizing type operations using the ``image type constructor
- FreshML: programming with binders made simple
- Homotopy type theory. Univalent foundations of mathematics
- Innovations in computational type theory using Nuprl
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Intuitionistic completeness of first-order logic
- Logic Programming
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Modified bar recursion
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories
- Nominal sets. Names and symmetry in computer science
- Nominal system T
- Non-extensional equality
- Nuprl's class theory and its applications
- On the computational content of the axiom of choice
- On the foundations of constructive mathematics -- especially in relation to the theory of continuous functions
- On weak completeness of intuitionistic predicate logic
- Programming with algebraic effects and handlers
- Relating two semantics of locally scoped names
- THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
- The continuum hypothesis in intuitionism
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- Towards a formally verified proof assistant
- Towards nominal computation
- Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Typed Dynamic Control Operators for Delimited Continuations
- Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
- When is a functional program not a functional program?
Cited in
(8)- scientific article; zbMATH DE number 7199581 (Why is no real title available?)
- scientific article; zbMATH DE number 7269245 (Why is no real title available?)
- Bar induction. The good, the bad, and the ugly
- Formally computing with the non-computable
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- Exercising Nuprl's open-endedness
- \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
- Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
This page was built for publication: Validating Brouwer's continuity principle for numbers using named exceptions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4640313)
