统一线性性和依赖性分析
摘要：线性和依赖性分析在计算机科学的几个应用中起着关键作用，特别是在资源管理和信息流控制方面。连接这些分析的是它们都需要对至少两个不同且相互约束的世界进行建模。尽管线性和依赖性分析解决了类似的问题，但是使用了不同的方法进行分析。对于线性分析，类型系统采用了Girard的线性逻辑中的共模指数模态。对于依赖分析，类型系统采用了Moggi的计算元语言中的单模态。由于这种方法上的差异，尽管理论上和实践上都希望将这两种分析统一起来，但并不简单。 幸运的是，随着分级上下文类型系统的最新进展，人们意识到线性和依赖性分析可以通过同一种方式来看待。然而，现有的分级上下文类型系统还不能完全统一线性和依赖性分析。现有的分级上下文类型系统存在问题，因为尽管它们的线性分析是通用的，但是它们的依赖性分析是有限的，主要是因为它们使用的分级模态是共模态而不是单模态。在本文中，我们通过有系统地扩展现有的分级上下文类型系统来解决这个限制，使得分级模态既是共模态又是单模态。这个扩展使我们能够将线性分析与通用的依赖性分析统一起来。我们提出了一个统一的线性依赖性演算，LDC，在任意纯类型系统中使用相同的机制进行线性和依赖性分析。我们证明了LDC是一个通用的线性和依赖性演算，它将个别分析的标准演算包含在内。
作者：Pritam Choudhury
论文ID：2304.03175
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-07