论文标题
类型检查数据结构比树木更复杂
Type checking data structures more complex than trees
论文作者
论文摘要
图是一个广义概念，它比树木更复杂的数据结构，例如差异列表，双连接列表，跳过列表和叶子连接的树。通常，这些结构用破坏性的分配来处理堆，这与纯粹的功能编程样式相反，并使验证变得困难。我们提出了一种新的纯粹功能性语言，$λ_{gt} $，将图形作为不可变的，一流的数据结构，具有基于图形转换的模式匹配机制，并开发了一种新的类型系统，$ f_ {gt} $用于该语言。我们的方法与使用分离逻辑，形状分析等对指针操纵程序进行分析相反。在（i）中，我们不考虑破坏性操作，而是由新的高级语言提供的图形上的模式匹配，该语言抽象指针和大量堆积了，并且（ii）（ii）我们可以自动地使用相当简单的型号来建立哪些属性。
Graphs are a generalized concept that encompasses more complex data structures than trees, such as difference lists, doubly-linked lists, skip lists, and leaf-linked trees. Normally, these structures are handled with destructive assignments to heaps, which is opposed to a purely functional programming style and makes verification difficult. We propose a new purely functional language, $λ_{GT}$, that handles graphs as immutable, first-class data structures with a pattern matching mechanism based on Graph Transformation and developed a new type system, $F_{GT}$, for the language. Our approach is in contrast with the analysis of pointer manipulation programs using separation logic, shape analysis, etc. in that (i) we do not consider destructive operations but pattern matchings over graphs provided by the new higher-level language that abstract pointers and heaps away and that (ii) we pursue what properties can be established automatically using a rather simple typing framework.
