Partial Elements and Recursion via Dominances in Univalent Type Theory

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

Authors

Colleges, School and Institutes

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.

Details

Original languageEnglish
Title of host publicationProceedings of 26th EACSL Annual Conference on Computer Science Logic (CSL2017)
EditorsValentin Goranko, Mads Dam
Publication statusPublished - Sep 2017
Event26th EACSL Annual Conference on Computer Science Logic (CSL 2017) - Stockholm, Sweden
Duration: 20 Aug 201724 Aug 2017
https://www.math-stockholm.se/en/konferenser-och-akti/logic-in-stockholm-2/26th-eacsl-annual-co

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl
Volume82
ISSN (Electronic)1868-8969

Conference

Conference26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Abbreviated titleCSL 2017
CountrySweden
CityStockholm
Period20/08/1724/08/17
Internet address

Keywords

  • univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory