Formally computing with the non-computable

DOI10.1007/978-3-030-80049-9_12OpenAlexW3179375897MaRDI QIDQ2117773

Liron Cohen

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80049-9_12

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Coq
• Nuprl

Cites Work

• 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
• Innovations in computational type theory using Nuprl
• Constructivism in mathematics. An introduction. Volume II
• Towards a Formally Verified Proof Assistant
• L.E.J. Brouwer – Topologist, Intuitionist, Philosopher
• Interacting with Modal Logics in the Coq Proof Assistant
• An interpretation of intuitionistic analysis
• Validating Brouwer's continuity principle for numbers using named exceptions
• Arguments for the Continuity Principle
• Computability Beyond Church-Turing via Choice Sequences
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• Bar Induction is Compatible with Constructive Type Theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• The Independence of Markov's Principle in Type Theory.
• A note on Bar Induction in Constructive Set Theory
• On weak completeness of intuitionistic predicate logic
• An Unsolvable Problem of Elementary Number Theory

This page was built for publication: Formally computing with the non-computable