Scopes as types
Scopes as types
复制标题
范围作为类型
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
E. Visser
中科院分区：
文献类型：
--
作者：
H. V. Antwerpen;Casper Bach Poulsen;A. Rouvoet;E. Visser
作用域图是一个很有前途的通用框架，可以对编程语言的绑定结构进行建模，连接形式化和实现，支持类型检查器的定义和类型安全证明的自动化。然而，以前的工作范围图已限于简单的，名义上的类型系统。在本文中，我们表明，查看范围的类型，使我们能够在一系列的非简单类型系统（包括结构记录和泛型类）使用范围的通用表示模型的内部结构的类型。此外，我们表明，这些类型之间的关系可以表示在广义范围图查询。我们扩展范围图与范围的关系和查询。我们介绍Statix，一个新的特定领域的元语言的规范的静态语义，范围图和约束的基础上。我们评估的范围作为类型的方法和Statix设计的简单类型的lambda演算的记录，系统F和轻量级泛型Java的案例研究。
Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.