Typed closure conversion for the calculus of constructions
Typed closure conversion for the calculus of constructions
复制标题
构造演算的类型化闭包转换
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Amal J. Ahmed
中科院分区：
文献类型：
--
作者：
W. J. Bowman;Amal J. Ahmed
依赖性的语言（例如COQ）用于指定和验证源程序的完整功能正确性 - 依赖类型的汇编本质上是很难的，问题是围绕高级组成的抽象来决定类型检查，但汇编干涉了针对运行时术语的类型系统规则开发一种具有强依赖对（σ类型）的结构计算（CC）的构造（CC）（COQ的核心语言的子集）到类型为安全的，依赖性的编译器中间语言，名为CC-CC这项工作中的核心挑战是如何将有关功能推理的源类型规则转换为目标类型系统规则，以证明这些规则是合理的。除了类型保存外，我们还证明了单独的汇编的正确性。
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms. We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs (Σ types)—a subset of the core language of Coq—to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.
可以改变世界的成功清单
DOI：
10.1007/978-3-319-30936-1_2
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Atkey R
通讯作者：
Atkey R