University of Birmingham > Talks@bham > Theoretical computer science seminar > Inductive Continuity via Brouwer Trees

Inductive Continuity via Brouwer Trees

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

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

Zoom details


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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.