Reachability types: tracking aliasing and separation in higher-order functional programs
Reachability types: tracking aliasing and separation in higher-order functional programs
复制标题
可达性类型：跟踪高阶函数程序中的别名和分离
DOI：
10.1145/3485516
复制
发表时间：
2021
影响因子：
--
通讯作者：
Rompf, Tiark
中科院分区：
文献类型：
--
作者：
Bao, Yuyan;Wei, Guannan;Bračevac, Oliver;Jiang, Yuxuan;He, Qiyang;Rompf, Tiark
所有权类型系统基于强制唯一访问路径的思想，主要关注对象和顶级类。然而，现有的模型并不容易反映嵌套的词法作用域，捕获，或逃逸闭包在高阶函数式编程模式，这是越来越多地采用，甚至在主流的面向对象语言的更好的方面。我们提出了一个新的类型系统，λ*，它使表达所有权风格的推理跨高阶函数。它通过可达集来跟踪共享和分离，并在其上分层额外的机制来选择性地实施唯一性。基于可达集，我们扩展了具有表达性的流敏感效果系统的类型系统，从而实现了移动语义和所有权转移。此外，我们提出了几个案例研究和扩展，包括应用程序的代数效果，一杆延续，和安全的并行化的能力。
Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ*, which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.
登录
查看更多内容
DOI：
--
发表时间：
2016
期刊：
European Conference on Object-Oriented Programming
影响因子：
--
作者：
Elias Castegren;Tobias Wrigstad
通讯作者：
Tobias Wrigstad
用于对象初始化的类型和效果系统
DOI：
--
发表时间：
2020
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Fengyun Liu;Ondřej Lhoták;Aggelos Biboudis;Paolo G. Giarrusso;Martin Odersky
通讯作者：
Martin Odersky
可达性和非循环性的类型系统
DOI：
--
发表时间：
2005
期刊：
European Conference on Object-Oriented Programming
影响因子：
--
作者：
Yi Lu;John Michael Potter
通讯作者：
John Michael Potter
依赖对象类型 (DOT) 的类型健全性
DOI：
--
发表时间：
2016
期刊：
Conference on Object-Oriented Programming Systems, Languages, and Applications
影响因子：
--
作者：
Tiark Rompf;Nada Amin
通讯作者：
Nada Amin
重新审视干扰的句法控制
DOI：
10.1016/s1571-0661(04)00026-x
发表时间：
1999
期刊：
2009 24th Annual IEEE Symposium on Logic In Computer Science
影响因子：
--
作者：
P. O'Hearn;J. Power;R. D. Tennent;M. Takeyama
通讯作者：
M. Takeyama