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.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 147–160. POPL ’99, Association for Computing Machinery, New York, NY, USA (1999). https://doi.org/10.1145/292540.292555
Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). https://doi.org/10.1145/3408972
Abel, A., Scherer, G.: On irrelevance and algorithmic equality in predicative type theory. Logical Methods in Computer Science 8(1) (mar 2012). https://doi.org/10.2168/lmcs-8(1:29)2012
Atkey, R.: Syntax and semantics of quantitative type theory. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. p. 56–65. LICS ’18, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209189
Barendregt, H.P.: Lambda Calculi with Types, p. 117–309. Oxford University Press Inc, USA (1993)
Barras, B., Bernardo, B.: The implicit calculus of constructions as a programming language with dependent types. In: Amadio, R. (ed.) Foundations of Software Science and Computational Structures. pp. 365–379. FOSSACS 2008, Springer, Berlin Heidelberg, Budapest, Hungary (2008)
Bernardy, J.P., Guilhem, M.: Type-theory in color. SIGPLAN Not. 48(9), 61–72 (Sep 2013). https://doi.org/10.1145/2544174.2500577
Brady, E.: Idris 2: Quantitative Type Theory in Practice. In: Møller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 194, pp. 9:1–9:26. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). https://doi.org/10.4230/LIPIcs.ECOOP.2021.9
Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 351–370. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
Choudhury, P., Eades III, H., Eisenberg, R.A., Weirich, S.: A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang. 5(POPL) (Jan 2021). https://doi.org/10.1145/3434331
Choudhury, P., Eades III, H., Weirich, S.: Artifact associated with "A Dependent Dependency Calculus" (Jan 2022). https://doi.org/10.5281/zenodo.5903726
Choudhury, P., Eades III, H., Weirich, S.: A dependent dependency calculus (extended version) (2022), https://arxiv.org/abs/2201.11040
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (May 1976). https://doi.org/10.1145/360051.360056
Eisenberg, R.A., Duboc, G., Weirich, S., Lee, D.: An existential crisis resolved: Type inference for first-class existential types. Proc. ACM Program. Lang. 5(ICFP) (Aug 2021), https://richarde.dev/papers/2021/exists/exists.pdf
Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: European Symposium on Programming Languages and Systems. pp. 331–350. Springer (2014)
Heintze, N., Riecke, J.G.: The slam calculus: Programming with secrecy and integrity. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 365–377. POPL ’98, Association for Computing Machinery, New York, NY, USA (1998). https://doi.org/10.1145/268946.268976
Lourenço, L., Caires, L.: Dependent information flow types. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 317–328. POPL ’15, Association for Computing Machinery, New York, NY, USA (2015). https://doi.org/10.1145/2676726.2676994
McBride, C.: I Got Plenty o’ Nuttin’, pp. 207–233. Springer International Publishing, Cham (2016)
Miquel, A.: The implicit calculus of constructions extending pure type systems with an intersection type binder and subtyping. In: Abramsky, S. (ed.) Typed Lambda Calculi and Applications. pp. 344–359. Springer Berlin Heidelberg, Berlin, Heidelberg (2001)
Mishra-Linger, N., Sheard, T.: Erasure and polymorphism in pure type systems. In: Proceedings of the Theory and Practice of Software, 11th International Conference on Foundations of Software Science and Computational Structures. p. 350–364. FOSSACS’08/ETAPS’08, Springer-Verlag, Berlin, Heidelberg (2008)
Mishra-Linger, R.N.: Irrelevance, Polymorphism, and Erasure in Type Theory. Ph.D. thesis, Portland State University, Department of Computer Science (2008). https://doi.org/10.15760/etd.2669
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991), https://www.sciencedirect.com/science/article/pii/0890540191900524, selections from 1989 IEEE Symposium on Logic in Computer Science
Moon, B., Eades III, H., Orchard, D.: Graded modal dependent type theory. In: Yoshida, N. (ed.) Programming Languages and Systems. pp. 462–490. Springer International Publishing, Cham (2021)
Nuyts, A., Devriese, D.: Degrees of relatedness: A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09–12, 2018. pp. 779–788. ACM (2018). https://doi.org/10.1145/3209108.3209119,https://doi.org/10.1145/3209108
Orchard, D., Liepelt, V.B., Eades III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https://doi.org/10.1145/3341714
Petricek, T., Orchard, D., Mycroft, A.: Coeffects: A calculus of context-dependent computation. In: Proceedings of International Conference on Functional Programming. ICFP 2014 (2014)
Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. pp. 221–. LICS ’01, IEEE Computer Society, Washington, DC, USA (2001), http://dl.acm.org/citation.cfm?id=871816.871845
Prost, F.: A static calculus of dependencies for the \(\lambda \)-cube. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332). pp. 267–276 (2000). https://doi.org/10.1109/LICS.2000.855775
Shikuma, N., Igarashi, A.: Proving noninterference by a fully complete translation to the simply typed \(\lambda \)-calculus. In: Proceedings of the 11th Asian Computing Science Conference on Advances in Computer Science: Secure Software and Related Issues. p. 301–315. ASIAN’06, Springer-Verlag, Berlin, Heidelberg (2006)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 355–364. POPL ’98, Association for Computing Machinery, New York, NY, USA (1998). https://doi.org/10.1145/268946.268975
Sulzmann, M., Chakravarty, M.M.T., Jones, S.P., Donnelly, K.: System f with type equality coercions. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. p. 53–66. TLDI ’07, Association for Computing Machinery, New York, NY, USA (2007). https://doi.org/10.1145/1190315.1190324
Tejiščák, M.: A dependently typed calculus with pattern matching and erasure inference. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). https://doi.org/10.1145/3408973
Thiemann, P.: A unified framework for binding-time analysis. In: Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development. p. 742–756. TAPSOFT ’97, Springer-Verlag, Berlin, Heidelberg (1997)
Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3 (1995)
Weirich, S., Voizard, A., de Amorim, P.H.A., Eisenberg, R.A.: A specification for dependent types in Haskell. Proc. ACM Program. Lang. 1(ICFP), 31:1–31:29 (Aug 2017). https://doi.org/10.1145/3110275
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Choudhury, P., Eades, H., Weirich, S. (2022). A Dependent Dependency Calculus. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-99336-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99335-1
Online ISBN: 978-3-030-99336-8
eBook Packages: Computer ScienceComputer Science (R0)