一句话：本文用范畴论中 monadic 与 comonadic 思想设计统一依赖分析演算，涵盖并解释 DCC 与 λ∘。
依赖分析对安全信息流、绑定时间分析等至关重要。Abadi 等人将多种演算统一为 Dependency Core Calculus (DCC)，但其 monadic bind 规则非标准，依赖辅助 protection judgement，且因 monadic 本质无法刻画 comonadic 依赖分析，如 Davies 的 binding-time calculus λ∘。本文受范畴论标准思想启发，设计一种新的依赖演算，兼具 monadic 与 comonadic 特征，可涵盖 DCC 与 λ∘。该构造用范畴概念解释 DCC 的非标准 bind 规则和 protection judgement，并导出一种证明依赖分析正确性的新技术。作者用此技术给出 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 λ ∘ .