Validating Brouwer's continuity principle for numbers using named exceptions

DOI10.1017/S0960129517000172zbMATH Open1390.68584OpenAlexW2765145981MaRDI QIDQ4640313FDOQ4640313

Authors: Vincent Rahli, Mark Bickford 

Publication date: 17 May 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129517000172

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Intuitionistic mathematics (03F55) Constructive and recursive analysis (03F60)

Cites Work

• Innovations in computational type theory using Nuprl
• Edinburgh LCF. A mechanized logic of computation
• Programming with algebraic effects and handlers
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Continuity of Gödel's system T definable functionals via effectful forcing
• When is a functional program not a functional program?
• Nominal sets. Names and symmetry in computer science
• A dependent nominal type theory
• Title not available (Why is that?)
• A note on forcing and type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Computational Interpretation of Forcing in Type Theory
• On weak completeness of intuitionistic predicate logic
• Homotopy Type Theory: Univalent Foundations of Mathematics
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Towards a Formally Verified Proof Assistant
• Title not available (Why is that?)
• Title not available (Why is that?)
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• A Constructive Model of Uniform Continuity
• Computing with Functionals—Computability Theory or Computer Science?
• Towards nominal computation
• Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
• On the computational content of the axiom of choice
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Type classes for efficient exact real arithmetic in Coq
• Title not available (Why is that?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Constructive set theory and Brouwerian principles
• Nuprl's class theory and its applications
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Intuitionistic completeness of first-order logic
• Title not available (Why is that?)
• On the foundations of constructive mathematics -- especially in relation to the theory of continuous functions
• Title not available (Why is that?)
• Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
• Title not available (Why is that?)
• Modified bar recursion
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• Exhaustible sets in higher-type computation
• A note on Bar Induction in Constructive Set Theory
• Forcing in Proof Theory
• Logic Programming
• BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
• Title not available (Why is that?)
• FreshML
• A dependent type theory with abstractable names
• Computer Science Logic
• Computational foundations of basic recursive function theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Arguments for the Continuity Principle
• Title not available (Why is that?)
• Title not available (Why is that?)
• Typed Dynamic Control Operators for Delimited Continuations
• A simple nominal type theory
• A constructive logic behind the catch and throw mechanism
• Dependent Types for Nominal Terms with Atom Substitutions
• The continuum hypothesis in intuitionism
• Title not available (Why is that?)
• An intuitionistic λ-calculus with exceptions
• Title not available (Why is that?)
• Nominal system T
• Title not available (Why is that?)
• Formalizing Type Operations Using the “Image” Type Constructor
• Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
• Relating two semantics of locally scoped names
• A fresh look at programming with names and binders
• Non-extensional equality
• A type system for call-by-name exceptions
• A System F with Call-by-Name Exceptions

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Formally computing with the non-computable
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity

Uses Software

• Coq
• MetaPRL
• Nuprl
• Freshml
• Agda
• Irdis
• Idris
• Eff

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)