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
- 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
- Forcing in Type Theory
- Southern Logic Seminar
- 23 February 2023
- abstract, slides