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

I am looking into phase distinctions in type theory as a way of internalising the compilation pipeline, for low-level and type-safe control over generated code. I like a structural approach based on SOGATs.

On the side, I am tinkering with optimising large-scale computation graphs, through rewriting, sparsification, quantisation, and custom vectorisation techniques. Why? Mostly because it’s fun. But also because AI poses a huge environmental challenge.

Papers, abstracts & presentations

  1. Type Theory with Erasure. Constantine Theocharis, Edwin Brady. Preprint, Feb 2026. [preprint]
  2. Natural Models for Computational Irrelevance. Constantine Theocharis. SPLS Dec 2025. [slides]
  3. Unboxed Dependent Types. Constantine Theocharis, Ellis Kesterton. TYPES 2025. [video] [slides] [abstract]
  4. Custom Representations of Inductive Families. Constantine Theocharis, Edwin Brady. TFP 2025. [preprint] [published]
  5. Structural Refactorings for Exploring Dependently Typed Programming. Adam Barwell, Christopher Brown, Mun See Chang, Constantine Theocharis, Simon Thompson. TFP 2024. [published]