Research

I am interested in all things Curry-Howard-Lambek. From my background I am more comfortable with the type theory and categorical side of this correspondence, but Birmingham has been a good place to familiarise myself more with the proof theory side of things.

Currently my work focuses on computational views of choice sequences. Choice sequences were introduced by Brouwer in his second act of intuitionism as a means to develop a well-behaved constructive version of the real numbers and analysis. As it turns out, choice sequences can be seen as instances of forcing and Kripke/Beth semantics, and through this connection I am trying to find a nice setup for studying choice sequences through the lens of categorical realizability.

Publications

1. 1. Separating Markov's Principles
   2. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli
   3. LICS, 2024
   4. doi
2. 1. Inductive Continuity via Brouwer Trees
   2. Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, Ayberk Tosun
   3. MFCS, 2023
   4. doi

Extended Abstracts

1. 1. Limited Principles of Omniscience in Constructive Type Theory
   2. Bruno da Rocha Paiva, Liron Cohen, Yannick Forster, Dominik Kirst, Vincent Rahli
   3. TYPES, 2024
   4. pdf
2. 1. Markov’s Principles in Constructive Type Theory
   2. Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
   3. TYPES, 2023
   4. pdf

Theses

1. 1. A Model-Theoretic Study of Allen's Interval Algebra
   2. MEng thesis at Imperial College London, Jul 2022
   3. pdf, bibtex

Talks

1. 1. Separating Markov's Principles
   2. LICS, Jul 2024
   3. slides
2. 1. Limited Principles of Omniscience in Constructive Type Theory
   2. TYPES, Jun 2024
   3. slides
3. 1. Timeful Mathematics via Brouwer's Choice Sequences
   2. Birmingham Facts and Snacks Seminar, Feb 2024
   3. abstract, slides
4. 1. Forcing in Type Theory
   2. Southern Logic Seminar, Feb 2023
   3. abstract, slides