依赖分析的单子和余单子方面
摘要：依赖分析在计算机科学中的一些应用中是至关重要的。它是安全信息流分析、绑定时间分析等的关键。文献中已经提出了各种计算方法来分析各个依赖关系。通过扩展Moggi的单子元语言，Abadi等人将其中几个计算方法统一成了依赖核心演算（DCC）。DCC在过去的二十年中作为依赖分析的基础框架发挥了重要作用。然而，尽管成功，DCC也有局限性。首先，这个演算的单子绑定规则是非标准的，依赖于辅助的保护判断。其次，作为单子的性质，该演算无法捕捉到具有共单子性质的依赖分析，例如Davies的绑定时间演算$lambda^circ$。在本文中，我们通过设计一个受范畴论中标准思想启发的替代性依赖演算来解决这些局限性。我们的演算既是单子的又是共单子的，并包含了DCC和$lambda^circ$。我们的构造以标准范畴概念的方式解释了DCC的非标准绑定规则和保护判断。它还导致了一种用于证明依赖分析正确性的新技术。我们利用这种技术提出了DCC和$lambda^circ$的替代正确性证明。
作者：Pritam Choudhury
论文ID：2209.06334
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-15