Computability beyond Church-Turing via choice sequences

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Computability beyond Church-Turing via choice sequences. / Bickford, Mark; Cohen, Liron; Constable, Robert L.; Rahli, Vincent.

LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), 2018. p. 245-254.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Bickford, M, Cohen, L, Constable, RL & Rahli, V 2018, Computability beyond Church-Turing via choice sequences. in LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), pp. 245-254, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209200

APA

Bickford, M., Cohen, L., Constable, R. L., & Rahli, V. (2018). Computability beyond Church-Turing via choice sequences. In LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 245-254). Association for Computing Machinery (ACM). https://doi.org/10.1145/3209108.3209200

Vancouver

Bickford M, Cohen L, Constable RL, Rahli V. Computability beyond Church-Turing via choice sequences. In LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM). 2018. p. 245-254 https://doi.org/10.1145/3209108.3209200

Author

Bickford, Mark ; Cohen, Liron ; Constable, Robert L. ; Rahli, Vincent. / Computability beyond Church-Turing via choice sequences. LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), 2018. pp. 245-254

Bibtex

@inproceedings{259f38efc3864b7386cae739ed278549,
title = "Computability beyond Church-Turing via choice sequences",
abstract = "Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl. ",
author = "Mark Bickford and Liron Cohen and Constable, {Robert L.} and Vincent Rahli",
year = "2018",
month = jul,
day = "9",
doi = "10.1145/3209108.3209200",
language = "English",
isbn = "978-1-4503-5583-4",
pages = "245--254",
booktitle = "LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",
note = "33rd Annual ACM/IEEE Symposium on Logic in Computer Science ; Conference date: 09-07-2018 Through 12-07-2018",

}

RIS

TY - GEN

T1 - Computability beyond Church-Turing via choice sequences

AU - Bickford, Mark

AU - Cohen, Liron

AU - Constable, Robert L.

AU - Rahli, Vincent

PY - 2018/7/9

Y1 - 2018/7/9

N2 - Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.

AB - Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.

U2 - 10.1145/3209108.3209200

DO - 10.1145/3209108.3209200

M3 - Conference contribution

SN - 978-1-4503-5583-4

SP - 245

EP - 254

BT - LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery (ACM)

T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 9 July 2018 through 12 July 2018

ER -