TY - GEN
T1 - A Dependent Dependency Calculus
AU - Choudhury, Pritam
AU - Eades, Harley
AU - Weirich, Stephanie
N1 - 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 -