Dependent Type Systems as Macros
Dependent Type Systems as Macros
复制标题
DOI：
10.1145/3371071
复制
发表时间：
2020-01-01
影响因子：
1.8
通讯作者：
Bowman, William J.
中科院分区：
文献类型：
--
作者：
Chang, Stephen;Ballantyne, Michael;Bowman, William J.
我们提出了TURNSTILE+，一个高层次的，基于宏的MetaDSL构建依赖类型的语言。有了它，程序员可以快速地原型化和重新设计新的依赖类型的功能和扩展。或者，它们可以创建全新的DSL，其依赖类型“power”是针对特定域定制的。我们的框架对面向语言编程的支持也使其适合于实验交互组件的系统，例如，一个证明助手及其配套DSL。本文解释了TURNSTILE+的实现细节，以及如何使用它来创建各种依赖类型的语言，从一个轻量级的索引类型，到一个全谱证明助手，完成了一个战术系统和扩展功能，如大小类型和SMT交互。
We present TURNSTILE+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create entirely new DSLs whose dependent type "power" is tailored to a specific domain. Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs. This paper explains the implementation details of TURNSTILE+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.