一句话：为带反向模式微分的可微分编程语言建立操作语义与指称语义，并证明二者一致。
自动微分在科学计算与机器学习中广泛使用，但其不同实现与数学导数概念的关系常不清晰，甚至可能出现偏差。为在编程语境中研究自动微分，作者定义了一个小而富有表达力的可微分编程语言，包含反向模式微分构造。论文分别给出操作语义和指称语义：操作语义采用常见实现技术，指称语义采用实分析中的微分概念。关键结果是证明这两种语义相互一致，从而把实现技术与数学导数语义联系起来，为自动微分系统提供语义基础。
Automatic differentiation plays a prominent role in scientific computing and in modern machine learning, often in the context of powerful programming systems. The relation of the various embodiments of automatic differentiation to the mathematical notion of derivative is not always entirely clear---discrepancies can arise, sometimes inadvertently. In order to study automatic differentiation in such programming contexts, we define a small but expressive programming language that includes a construct for reverse-mode differentiation. We give operational and denotational semantics for this language. The operational semantics employs popular implementation techniques, while the denotational semantics employs notions of differentiation familiar from real analysis. We establish that these semantics coincide.