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.

翻译：我们提出Turnstile+, 是一个高层次、 宏观的元DSL, 用于建立依赖打字的语言。 程序员可以快速地对新打字的功能和扩展进行原型和循环设计。 或者他们可以创建全新DSL, 其依赖型号“ 能力” 适合特定领域。 我们的框架支持面向语言的编程也使得它适合实验交互式组件系统, 如校对助理及其配套的DSL。 本文解释了 Turnstile+ 的实施细节, 以及它可能如何用来创建大量依赖打字的语言, 从有索引型的轻量级语言到全频谱校准助理, 配有大小类型和 SMT 互动特征的战术系统和扩展。