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. 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. 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. Timeful Mathematics via Brouwer's Choice Sequences
   2. Birmingham Facts and Snacks Seminar
   3. 8 February 2024
   4. abstract, slides
2. 1. Forcing in Type Theory
   2. Southern Logic Seminar
   3. 23 February 2023
   4. abstract, slides