Type Automata

PL researchers have a profound understanding of automata theory but fail to grasp the subtleties and nuances of the type systems used in modern programming languages. My research pursues new insights into the computational power of type systems by connecting them with well-founded classes of automata through type automata---machines that employ program types as control and storage. In addition, I demonstrate advanced type-level metaprogramming applications of type automata that coerce the compiler into performing computations at compile time.