A Dependent Dependency Calculus
A Dependent Dependency Calculus
复制标题
依赖依赖演算
DOI：
10.1007/978-3-030-99336-8_15
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Weirich, Stephanie
中科院分区：
文献类型：
--
作者：
Choudhury, Pritam;Eades III, Harley;Weirich, Stephanie
二十多年前，阿巴迪等人。建立了依赖项核心演算(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 typechecking and program execution.