2026-07-20T05:41:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7682 2024-03-12T11:58:22Z ddc:004 open_access

Partial Elements and Recursion via Dominances in Univalent Type Theory Escardó, Martín H. Knapp, Cory M. univalent type theory homotopy type theory partial function dominance recursion theory computability theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martín H. Escardó and Cory M. Knapp 2017 Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2017.21 urn:nbn:de:0030-drops-76822 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21 eng https://creativecommons.org/licenses/by/3.0/legalcode