论文标题
依赖依赖性计算（扩展版）
A Dependent Dependency Calculus (Extended Version)
论文作者
论文摘要
二十多年前，Abadi等人。建立了依赖关系核心演算（DCC），作为分析类型编程语言依赖关系的通用框架。从那时起，依赖性分析已显示出对语言设计的许多实际好处：其结果可以帮助用户和编译器执行安全限制，消除死亡代码以及其他应用程序。在这项工作中，我们提出了一个依赖性依赖性计算（DDC），该计算将这一总体思想扩展到相关语言的设置。我们使用此计算来跟踪运行时和编译时无关，从而更快地进行了类型检查和程序执行。
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.
