Constantine Theocharis

Kωνσταντίνος Θεοχάρης ⋅ /ˈkɒnstəntiːn θe.oˈhäːris/

I am a PhD student at the University of St Andrews, working on type theory for programming languages. I am supervised by Edwin Brady.

My academic interests include type theory, its formalisation, category theory, low-level verification, metaprogramming, optimisations, compiler design, and elaboration.

github ⋅ mastodon ⋅ orcid ⋅ st-andrews ⋅ linkedin ⋅ scholar

My academic email can be found at the st-andrews link above.

What I am working on

  1. Phase distinctions in type theory as a way of internalising the compilation pipeline, for low-level and type-safe control over generated code.
  2. A secret project that will hopefully save me from writing more toy compilers for some time.
  3. Understanding aspects of 2-category theory.

Papers, abstracts & talks

  • Phase Your Compilation (talk). TRIPLE 2026. [slides]
  • Type Theory with Erasure (paper). FSCD 2026, with Edwin Brady. [preprint]
  • Natural Models for Computational Irrelevance (talk). SPLS Dec. 2025. [slides]
  • Unboxed Dependent Types (extended abstract). TYPES 2025, with Ellis Kesterton. [video] [slides] [abstract]
  • Custom Representations of Inductive Families (paper). TFP 2025, with Edwin Brady. [preprint] [published]
  • Structural Refactorings for Exploring Dependently Typed Programming (paper). TFP 2024, with Adam Barwell, Christopher Brown, Mun See Chang, Simon Thompson. [published]