Computability beyond Church-Turing via choice sequences

DOI10.1145/3209108.3209200MaRDI QIDQ5145297zbMATH OpenOpenAlexWikidataFDO

Authors Mark Bickford, Liron Cohen, Vincent Rahli, Robert Constable

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL http://pure-oai.bham.ac.uk/ws/files/71146432/Computability_Beyond.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Metamathematics of constructive systems (03F50) Other degrees and reducibilities in computability and recursion theory (03D30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Recommendations

• Exercising Nuprl's open-endedness
• Realizing Brouwer's sequences
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Computer Science Logic
• Publication:4934288

Cited in

(4)

• Formally computing with the non-computable
• scientific article; zbMATH DE number 4130139 (Why is no real title available?)
• The effects of effects on constructivism
• Higher order functions and Brouwer's thesis

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Computability beyond Church-Turing via choice sequences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145297)