一句话：为 Dependent Haskell 提出核心语义与显式类型语言，并在 Coq 中形式化类型安全及相关定理。
论文为在 Haskell 中加入完整谱系依赖类型（Dependent Haskell）提出核心语义规范。该语义包含两个相关语言：一个带非终止、无关参数和等式抽象的 Curry 风格依赖类型语言，以及受 GHC Core FC 启发、适合 GHC 实现的显式类型类似物。作者在 Coq 证明助手中形式化类型安全及连接两种语言的关键定理。因与 Haskell 向后兼容，类型安全在非终止计算存在时仍成立；但与 Coq、Agda、Idris 不同，非终止使 Haskell 项语言不对应一致逻辑。
We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler's core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results---chiefly, type safety, along with theorems that relate these two languages---have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell's term language does not correspond to a consistent logic.
@article{WeirichVAE17,
title = {A specification for dependent types in Haskell},
author = {Stephanie Weirich and Antoine Voizard and Pedro Henrique Azevedo de Amorim and Richard A. Eisenberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110275}
}