Abstract
We begin by revisiting partiality in univalent type theory via the notion of dominance. We then perform first steps in constructive computability theory, discussing the consequences of working with computability as property or structure, without assuming countable choice or Markov’s principle. A guiding question is what, if any, notion of partial function allows the proposition “all partial functions on natural numbers are Turing computable” to be consistent.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of 26th EACSL Annual Conference on Computer Science Logic (CSL2017) |
| Editors | Valentin Goranko, Mads Dam |
| Publisher | Schloss Dagstuhl |
| Number of pages | 16 |
| ISBN (Print) | 9781510847118 |
| DOIs | |
| Publication status | Published - Sept 2017 |
| Event | 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) - Stockholm, Sweden Duration: 20 Aug 2017 → 24 Aug 2017 https://www.math-stockholm.se/en/konferenser-och-akti/logic-in-stockholm-2/26th-eacsl-annual-co |
Publication series
| Name | Leibniz International Proceedings in Informatics (LIPIcs) |
|---|---|
| Publisher | Schloss Dagstuhl |
| Volume | 82 |
| ISSN (Electronic) | 1868-8969 |
Conference
| Conference | 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) |
|---|---|
| Abbreviated title | CSL 2017 |
| Country/Territory | Sweden |
| City | Stockholm |
| Period | 20/08/17 → 24/08/17 |
| Internet address |
Keywords
- univalent type theory
- homotopy type theory
- partial function
- dominance
- recursion theory
- computability theory