Computability beyond Church-Turing via choice sequences

DOI10.1145/3209108.3209200zbMATH Open1452.03133OpenAlexW2798735574WikidataQ130953758 ScholiaQ130953758MaRDI QIDQ5145297FDOQ5145297

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

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

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)

Cited In (4)

• Formally computing with the non-computable
• Title not available (Why is that?)
• The effects of effects on constructivism
• Higher order functions and Brouwer's thesis

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)