Inductive Continuity via Brouwer Trees

Add to your list(s) Download to your calendar using vCal

• Ayberk Tosun (University of Birmingham)
• Friday 25 August 2023, 14:00-14:50
• LG23, Computer Science // Zoom.

If you have a question about this talk, please contact George Kaye.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

This will be a dry run of my MFCS talk in which I will be presenting our work with Liron Cohen, Vincent Rahli, and Bruno da Rocha Paiva.

Here is the abstract of the paper :

Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, a stronger formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of the strong continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this stronger form of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that the strong continuity principle indeed implies other forms of continuity principles.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, Computer Science // Zoom
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.