A Dependent Dependency Calculus (Extended Version)

TL;DR

This paper introduces a Dependent Dependency Calculus (DDC) that extends dependency analysis to dependently-typed languages, improving type-checking efficiency and enabling better tracking of relevance at runtime and compile-time.

Contribution

It presents a novel calculus that extends the Dependency Core Calculus to dependently-typed languages, facilitating more precise dependency tracking and efficiency improvements.

Findings

Enables faster type-checking in dependently-typed languages

Tracks run-time and compile-time irrelevance effectively

Extends the theoretical framework of dependency calculus

Abstract

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.