I am a interested in Type theory, Logic, Category theory, Proof Assistants and Programming languages.

Talks

Raphaël Sterbac

TYPES (2026)

Experience

Research Internship, University of Cambridge (5 months)
- Under the supervision of Jon Sterling
- Foundational design and implementation of a new proof assistant based on homotopy type theory (“Project Pterodactyl”). Study and implementation of a new presentation for cumulative universes, and investigation of its semantics in toposes.
Research Internsip, Chalmers University of Technology (2 months)
- Under the supervision of Thierry Coquand.
- Syntax and semantics of dependent type theory: proving normalisation semantically with the Artin glueing technique, proving the equivalence of Tarski and Russell presentations for cumulative universes. More generally, I also related the PTS and GAT presentations for type theory in general, extending initiality results in the way of Streicher’s book.