复杂于树的数据结构的类型检查
摘要：图是一个广义的概念，涵盖比树更复杂的数据结构，如差异列表、双向链表、跳跃表和叶链接树。通常，这些结构都是通过对堆进行破坏性赋值来处理的，这与纯函数式编程风格相反，并且使验证变得困难。我们提出了一种新的纯函数式语言$lambda\_{GT}$，它将图作为不可变的一流数据结构处理，并具有基于图转换的模式匹配机制。我们还为该语言开发了一种新的类型系统$F\_{GT}$。我们的方法与使用分离逻辑、形状分析等分析指针操作程序的方法相反，因为(i)我们不考虑破坏性操作，而是利用新的更高级别的语言提供的图模式匹配抽象指针和堆，并且(ii)我们通过一种相当简单的类型框架来追求可以自动建立什么属性。
作者：Jin Sano, Naoki Yamamoto, Kazunori Ueda
论文ID：2209.05149
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-13