同步编程中多速率流的依赖类型
编程语言
2017-02-09 v1
摘要
同步编程语言在20世纪80年代作为实现反应式系统的工具而出现，这类系统与物理环境事件交互，并且常常必须在严格的时间约束下这样做。在本报告中，我们在 ATS 中编码了一种称为 Prelude 的实验性同步语言的各种实时原语，其中 ATS 是一种具有 ML 风格函数式核心的静态类型语言，支持依赖类型（DML 风格）和线性类型。我们展示了施加于这些原语的验证需求可以用 ATS 中的依赖类型形式化表达。此外，我们修改了 Prelude 编译器，以从 Prelude 源码自动生成 ATS 代码。这一修改后的编译器使我们能够仅依靠 ATS 中的类型检查来解除因类型检查 Prelude 代码而产生的证明义务。尽管 ATS 通常用作通用编程语言，我们在此证明它也可方便地用于支持具有较弱表达力类型的语言中的某些高级静态检查形式。
引用
@article{arxiv.1702.02282,
title = {Dependent Types for Multi-Rate Flows in Synchronous Programming},
author = {William Blair and Hongwei Xi},
journal= {arXiv preprint arXiv:1702.02282},
year = {2017}
}
备注
In Proceedings ML/OCaml 2015, arXiv:1702.01872