Validating Brouwer's continuity principle for numbers using named exceptions
From MaRDI portal
Publication:4640313
DOI10.1017/S0960129517000172zbMath1390.68584OpenAlexW2765145981MaRDI QIDQ4640313
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
Constructive and recursive analysis (03F60) Mechanization of proofs and logical operations (03B35) Intuitionistic mathematics (03F55)
Related Items
Uses Software
Cites Work
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories
- Continuity of Gödel's system T definable functionals via effectful forcing
- Intuitionistic completeness of first-order logic
- Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
- Programming with algebraic effects and handlers
- A dependent type theory with abstractable names
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Innovations in computational type theory using Nuprl
- Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
- Constructivism in mathematics. An introduction. Volume II
- Computational foundations of basic recursive function theory
- A constructive logic behind the catch and throw mechanism
- Edinburgh LCF. A mechanized logic of computation
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On the foundations of constructive mathematics -- especially in relation to the theory of continuous functions
- A Simple Nominal Type Theory
- When is a functional program not a functional program?
- Nominal Sets
- Towards a Formally Verified Proof Assistant
- A dependent nominal type theory
- Towards nominal computation
- A Note on Forcing and Type Theory
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A Type System For Call-By-Name Exceptions
- A System F with Call-by-Name Exceptions
- Exhaustible sets in higher-type computation
- The continuum hypothesis in intuitionism
- Non-extensional equality
- On the computational content of the axiom of choice
- An intuitionistic λ-calculus with exceptions
- Forcing in Proof Theory
- Arguments for the Continuity Principle
- Type classes for efficient exact real arithmetic in Coq
- Formalizing Type Operations Using the “Image” Type Constructor
- A fresh look at programming with names and binders
- BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
- A Computational Interpretation of Forcing in Type Theory
- Nominal system T
- FreshML
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- Dependent Types for Nominal Terms with Atom Substitutions
- A Constructive Model of Uniform Continuity
- Computer Science Logic
- Logic Programming
- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Typed Dynamic Control Operators for Delimited Continuations
- Computing with Functionals—Computability Theory or Computer Science?
- Modified bar recursion
- A note on Bar Induction in Constructive Set Theory
- Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
- THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
- On weak completeness of intuitionistic predicate logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
