Formally computing with the non-computable
From MaRDI portal
Publication:2117773
DOI10.1007/978-3-030-80049-9_12OpenAlexW3179375897MaRDI QIDQ2117773FDOQ2117773
Authors: Liron Cohen 
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80049-9_12
Cites Work
- Innovations in computational type theory using Nuprl
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Constructivism in mathematics. An introduction. Volume II
- L.E.J. Brouwer – Topologist, Intuitionist, Philosopher
- 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 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Arguments for the Continuity Principle
- The independence of Markov's principle in type theory
- Bar induction is compatible with constructive type theory
- Title not available (Why is that?)
- A verified theorem prover backend supported by a monotonic library
- Validating Brouwer's continuity principle for numbers using named exceptions
- Bar induction. The good, the bad, and the ugly
- Stack semantics of type theory
- 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)
