一句话：为纯函数式数据并行语言 Futhark 设计高阶模块系统，并在 Coq 中形式化其静态语义与编译期消除。
针对纯函数式数据并行数组语言 Futhark 在组织大型库和完整程序时缺乏模块抽象的问题，本文提出一种高阶模块系统。该模块语言在编译期被完全消除，但可用于库与程序的结构化组织。文章给出静态类型系统以及可证明终止的 elaboration 动态语义，将模块项翻译为底层目标语言项，并借助基于积、集合与有限映射的语义对象编码在 Coq 中形式化。该系统统一处理模块类型抽象与核心语言多态，并支持实用的模块组合形式。评估以形式化开发与语义性质证明为主，表明模块机制可在不引入运行时开销的情况下增强大规模函数式 GPU 编程的组织能力。
We present a higher-order module system for the purely functional data-parallel array language Futhark. The module language has the property that it is completely eliminated at compile time, yet it serves as a powerful tool for organizing libraries and complete programs. The presentation includes a static and a dynamic semantics for the language in terms of, respectively, a static type system and a provably terminating elaboration of terms into terms of an underlying target language. The development is formalised in Coq using a novel encoding of semantic objects based on products, sets, and finite maps. The module language features a unified treatment of module type abstraction and core language polymorphism and is rich enough for expressing practical forms of module composition.
@article{paperbot299,
title = {Static interpretation of higher-order modules in Futhark: functional GPU programming in the large},
author = {Martin Elsman and Troels Henriksen and Danil Annenkov and Cosmin E. Oancea},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236792}
}