Research

I am interested in dependent type theories, constructive logic and categorical logic. Currently I am focused on using computational effects such as state or exceptions in dependent type theories to prove internally certain constructive principles such as Brouwer's continuity principle or Markov's principle. I am also interested in model theory and modal logic, although not so focused on these anymore.

Publications

1. 1. Separating Markov's Principles
   2. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli
   3. LICS 2024, Tallinn, Estonia, 2024
   4. doi
2. 1. Inductive Continuity via Brouwer Trees
   2. Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, Ayberk Tosun
   3. MFCS 2023, Bordeaux, France, 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, Copenhagen, Denmark 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, Valencia, Spain, 2023
   4. pdf

Theses

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

Talks

1. 1. Separating Markov's Principles
   2. LICS 2024
   3. 9 July 2024
   4. slides
2. 1. Separating Markov's Principles
   2. LICS 2024
   3. 9 July 2024
   4. slides
3. 1. Timeful Mathematics via Brouwer's Choice Sequences
   2. Birmingham Facts and Snacks Seminar
   3. 8 February 2024
   4. abstract, slides
4. 1. Forcing in Type Theory
   2. Southern Logic Seminar
   3. 23 February 2023
   4. abstract, slides