A Dependent Dependency Calculus (Extended Version)
Pritam Choudhury, Harley Eades III, Stephanie Weirich

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Logic, programming, and type systems · Distributed systems and fault tolerance
