Monadic and comonadic aspects of dependency analysis
Monadic and comonadic aspects of dependency analysis
复制标题
依赖分析的单子和共子方面
DOI：
10.1145/3563335
复制
发表时间：
2022
影响因子：
--
通讯作者：
Choudhury, Pritam
中科院分区：
文献类型：
--
作者：
Choudhury, Pritam
依赖性分析对于计算机科学中的多种应用至关重要。它是安全信息流分析、绑定时间分析等的本质。文献中已经提出了各种计算方法来分析个体依赖性。阿巴迪等。等人通过扩展 Moggi 的一元元语言，将其中一些演算统一到依赖核心演算（DCC）中。在过去的二十年里，DCC 一直是依赖性分析的基础框架。然而，尽管 DCC 取得了成功，但它也有其局限性。首先，微积分的一元绑定规则是非标准的，依赖于辅助保护判断。其次，由于具有单子性质，微积分无法捕获具有共子性质的依赖性分析，例如戴维斯的绑定时间演算 λ∘。在本文中，我们通过设计一种受范畴论标准思想启发的替代依赖演算来解决这些限制。我们的微积分本质上是单子和共子的，并且包含 DCC 和 λ∘。我们的构造用标准范畴概念解释了非标准绑定规则和DCC的保护判断。它还带来了一种证明依赖性分析正确性的新技术。我们使用这种技术来提供 DCC 和 λ∘ 正确性的替代证明。
Dependency analysis is vital to several applications in computer science. It lies at the essence of secure information flow analysis, binding-time analysis, etc. Various calculi have been proposed in the literature for analysing individual dependencies. Abadi et. al., by extending Moggi’s monadic metalanguage, unified several of these calculi into the Dependency Core Calculus (DCC). DCC has served as a foundational framework for dependency analysis for the last two decades. However, in spite of its success, DCC has its limitations. First, the monadic bind rule of the calculus is nonstandard and relies upon an auxiliary protection judgement. Second, being of a monadic nature, the calculus cannot capture dependency analyses that possess a comonadic nature, for example, the binding-time calculus, λ∘, of Davies. In this paper, we address these limitations by designing an alternative dependency calculus that is inspired by standard ideas from category theory. Our calculus is both monadic and comonadic in nature and subsumes both DCC and λ∘. Our construction explains the nonstandard bind rule and the protection judgement of DCC in terms of standard categorical concepts. It also leads to a novel technique for proving correctness of dependency analysis. We use this technique to present alternative proofs of correctness for DCC and λ∘.
登录
查看更多内容
DOI：
--
发表时间：
2019
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Maximilian Algehed;Jean
通讯作者：
Jean
结合时间分析的时间逻辑方法
DOI：
--
发表时间：
1995
期刊：
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Rowan Davies
通讯作者：
Rowan Davies
效果和单子的结合
DOI：
--
发表时间：
1998
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Jennifer S Peel;M. Mcnarry;S. Heffernan;V. Nevola;L. Kilduff;M. Waldron
通讯作者：
M. Waldron
使用 AST、Gensym 和 Reflection 实现多阶段语言
DOI：
--
发表时间：
2003
期刊：
International Conference on Generative Programming: Concepts and Experiences
影响因子：
--
作者：
Cristiano Calcagno;Walid Taha;Liwen Huang;X. Leroy
通讯作者：
X. Leroy
协同效应
DOI：
--
发表时间：
2014
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
T. Petříček;Dominic A. Orchard;A. Mycroft
通讯作者：
A. Mycroft