Research

My research concerns type theory, constructive mathematics, proof theory, and machine-checked formalization.

Formalized proof theory of modal logic

Together with Margherita Zorzi, I study proof systems for modal logic through formalization. One line uses position-based, or 2-sequent, proof systems for S4.2 and establishes cut elimination via Mix, the subformula property, consistency, completeness, and the finite model property. The NAMOR framework treats modal logics through systems parameterized by mode theories, including the axioms D, T, B, 4, 5, .2, .3, and .4.

Constructive and computable real analysis

In Cubical Agda, I work on constructive and computable real analysis: Cauchy completion, signed-digit representations, premetric spaces, and Lipschitz maps. This is joint work with Lorenzo Molena and Marcin Jan Turek-Grzybowski. The signed-digit and coinductive part builds on work with Thorsten Altenkirch.

Nuclei for substructural logics

Another line concerns conservation theorems for nuclei over substructural entailment relations, with Full Lambek logic as the setting. The results are formalized in Cubical Agda and connect to the CiE 2026 paper with Giulio Fellin, Tarmo Uustalu, and Cheng-Syuan Wan.

Categorical logic and normal forms

In categorical logic, I work on a canonical normal form theorem for the type theory of regular categories, within the modular correspondence of Maria Emilia Maietti, with whom this work is joint. The result has a complete Tait-style Agda formalization.

Research interests

Type theory, category theory, proof theory, constructive mathematics, computable real analysis, strong negation and apartness, proof assistants, minimal logic, modal logic, separation logic.