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 sheafification. This has meant I have ended up exploring the standard constructions of sheafification, logical incarnations for internal reasoning, and intensional tree-based views linking it to oracle computations. My current line of research in particular looks at sheafification in categorical realizability.

Publications

    1. Internal Effectful Forcing in System T
    2. Martín Escardó, Bruno da Rocha Paiva, Vincent Rahli and Ayberk Tosun
    3. FSCD, 2025
    4. doi
    1. Separating Markov's Principles
    2. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli
    3. LICS, 2024
    4. doi
    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. Realizability Triposes from Sheaves
    2. Bruno da Rocha Paiva, Vincent Rahli
    3. TYPES, 2025
    4. pdf
    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
    1. Markov’s Principles in Constructive Type Theory
    2. Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
    3. TYPES, 2023
    4. pdf

Talks

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

Theses

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