BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Partial functions and recursion via dominances in
univalent type theory - Cory Knapp
DTSTART:20170803T110000Z
DTEND:20170803T120000Z
UID:TALK2782AT
URL:/talk/index/2782
DESCRIPTION:We develop computability in a constructive univale
nt type theory\, without assuming countable choice
or Markov's principle\, paying special attention
to the handling of partiality in this setting via
the notion of dominance. During our development\,
we will consider the consequences of working with
computability as property or structure. A guiding
question is what\, if any\, notion of partial func
tion allows the proposition “all partial functions
on natural numbers are Turing computable” to be c
onsistent.\n\nThis is a practice talk for CSL 2017
.
LOCATION:CS 217
CONTACT:Dr Steve Vickers
END:VEVENT
END:VCALENDAR