Open Access 2022 | OriginalPaper | Chapter
A Dependent Dependency Calculus
Authors : Pritam Choudhury, Harley Eades III, Stephanie Weirich
Published in: Programming Languages and Systems
Publisher: Springer International Publishing
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.