Formally computing with the non-computable

DOI10.1007/978-3-030-80049-9_12MaRDI QIDQ2117773zbMATH OpenOpenAlexFDO

Authors 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)

Cites work

• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3552491 (Why is no real title available?)
• scientific article; zbMATH DE number 3573834 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 510786 (Why is no real title available?)
• scientific article; zbMATH DE number 1795233 (Why is no real title available?)
• scientific article; zbMATH DE number 2204804 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 3216177 (Why is no real title available?)
• scientific article; zbMATH DE number 3253161 (Why is no real title available?)
• A note on Bar Induction in Constructive Set Theory
• A verified theorem prover backend supported by a monotonic library
• An Unsolvable Problem of Elementary Number Theory
• An interpretation of intuitionistic analysis
• Arguments for the Continuity Principle
• Bar induction is compatible with constructive type theory
• Bar induction. The good, the bad, and the ugly
• Computability beyond Church-Turing via choice sequences
• Constructivism in mathematics. An introduction. Volume II
• Innovations in computational type theory using Nuprl
• Interacting with Modal Logics in the Coq Proof Assistant
• L.E.J. Brouwer – Topologist, Intuitionist, Philosopher
• On weak completeness of intuitionistic predicate logic
• Stack semantics of type theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• The independence of Markov's principle in type theory
• Towards a formally verified proof assistant
• Validating Brouwer's continuity principle for numbers using named exceptions

Cited in

(1)

• scientific article; zbMATH DE number 47574 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl
• Coq

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)