Computer Science PGR Seminar Constantine Theocharis: Type Theory with Erasure

All are welcome to listen to our speaker Constantine Theocharis.

Abstract: Programming languages with rich type systems can express strong correctness guarantees of programs. However, for rich enough type systems, this expressiveness comes at a cost: programs carry data that exists only to satisfy the type checker and serves no purpose at runtime. Erasure is a technique that identifies and removes such data during compilation. This results in efficient executables that still uphold these correctness guarantees.

Type theory provides a formal foundation for studying programming languages. It underlies all (reasonable) typed languages, including proof assistants. Although erasure is implemented in several such languages, its theoretical foundations remain underdeveloped. In this talk, I will present a new, structural formulation of erasure: unlike previous accounts, erasure arises from a uniform mechanism rather than being baked into every typing rule. As a result, it can be easily combined with other type theory features such as staging (type-safe metaprogramming). Many general results about type theory can now be directly reused to establish some useful properties of type checking and compilation, and inform their implementation. I will explain what this means and why it matters.

Bio: I am a third-year PhD student here, supervised by Edwin Brady. My research focuses on type theory, and in particular extensions of type theory that make it more suitable as a foundation for practical programming languages.