一句话：提出类型自动机，以程序类型为控制与存储，连接类型系统与自动机理论并支持类型级元编程。
该研究关注现代编程语言类型系统的计算能力及其微妙细节。作者指出，PL 研究者虽熟悉自动机理论，却往往难以把握类型系统的复杂行为。为此，论文提出“类型自动机”：一种以程序类型作为控制与存储的机器，通过它把类型系统与具有坚实基础的自动机类关联起来，从而获得关于类型系统计算能力的新洞见。论文还展示类型自动机的高级类型级元编程应用，使编译器在编译期执行计算。摘要未给出具体实验或基准评估，主要通过理论联系与应用示例论证其价值。
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.