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
- Separating Markov's Principles
- Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli
- LICS 2024, Tallinn, Estonia, 2024
- Inductive Continuity via Brouwer Trees
- Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, Ayberk Tosun
- MFCS 2023, Bordeaux, France, 2023
- doi
Extended Abstracts
- Markov’s Principles in Constructive Type Theory
- Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
- TYPES 2023, Valencia, Spain, 2023
- pdf
Theses
- A Model-Theoretic Study of Allen's Interval Algebra
- MEng thesis at Imperial College London
- July 2022
- pdf, bibtex
Talks
- Separating Markov's Principles
- LICS 2024
- 9 July 2024
- slides
- Timeful Mathematics via Brouwer's Choice Sequences
- Birmingham Facts and Snacks Seminar
- 8 February 2024
- abstract, slides
- Forcing in Type Theory
- Southern Logic Seminar
- 23 February 2023
- abstract, slides