TY - GEN
T1 - A Dependent Dependency Calculus
AU - Choudhury, Pritam
AU - Eades, Harley
AU - Weirich, Stephanie
N1 - Funding Information:
The first two authors were supported by the National Science Foundation under Grant Nos. 1703835 and 1521539. The second author was supported by the National Science Foundation under Grant No. 2104535.
Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Dependent Types
KW - Information Flow
KW - Irrelevance
UR - http://www.scopus.com/inward/record.url?scp=85128657683&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85128657683&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-99336-8_15
DO - 10.1007/978-3-030-99336-8_15
M3 - Conference contribution
AN - SCOPUS:85128657683
SN - 9783030993351
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 403
EP - 430
BT - Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
A2 - Sergey, Ilya
PB - Springer Science and Business Media Deutschland GmbH
T2 - 31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022
Y2 - 5 April 2022 through 7 April 2022
ER -