一句话：从内在类型化解释器出发，以类型导向的方式推导抽象机与编译器，并为简单表达式语言及STLC优化求值器展示该方法。
本文提出一种有原则的方法，用于推导抽象机及其配套编译器。该方法从内在类型化（intrinsically typed）的解释器出发，通过一系列类型导向的变换逐步得到抽象机与编译器，从而使正确性在构造过程中由类型保证。作者首先针对一个简单表达式语言详细展示了编译器推导的完整过程，随后重复该推导的前几步，为简单类型λ演算（STLC）得到一个优化求值器。该工作表明，类型信息不仅能指导程序编写，也能系统性地指导编译器与抽象机的构造，为编译器设计提供了一种可验证的推导路径。
Abstract This paper explores a principled approach to calculating abstract machines and associated compilers, starting from an intrinsically typed interpreter. After deriving a compiler for a simple expression language in some detail, the first steps of this calculation are repeated to derive an optimizing evaluator for the simply typed lambda calculus.