Formally computing with the non-computable
From MaRDI portal
Publication:2117773
DOI10.1007/978-3-030-80049-9_12OpenAlexW3179375897MaRDI QIDQ2117773FDOQ2117773
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80049-9_12
Cites Work
- 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?)
- 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?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Innovations in computational type theory using Nuprl
- On weak completeness of intuitionistic predicate logic
- Towards a Formally Verified Proof Assistant
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- Constructivism in mathematics. An introduction. Volume II
- L.E.J. Brouwer – Topologist, Intuitionist, Philosopher
- A note on Bar Induction in Constructive Set Theory
- An Unsolvable Problem of Elementary Number Theory
- Interacting with Modal Logics in the Coq Proof Assistant
- An interpretation of intuitionistic analysis
- Arguments for the Continuity Principle
- The Independence of Markov's Principle in Type Theory.
- Bar Induction is Compatible with Constructive Type Theory
- A Verified Theorem Prover Backend Supported by a Monotonic Library
- Validating Brouwer's continuity principle for numbers using named exceptions
- Computability Beyond Church-Turing via Choice Sequences
Cited In (1)
Uses Software
This page was built for publication: Formally computing with the non-computable
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117773)
