{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:01Z","timestamp":1775790781107,"version":"3.50.1"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720186","type":"print"},{"value":"9783030720193","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many such theories in recent years which equip a type theory with quantitative dataflow tracking, usually via a semiring-like structure which provides analysis on variables (often called \u2018quantitative\u2019 or \u2018coeffect\u2019 theories). We present Graded Modal Dependent Type Theory (<jats:sc>Grtt<\/jats:sc>for short), which equips a dependent type theory with a general, parameterizable analysis of the flow of data, both in and between computational terms and types. In this theory, it is possible to study, restrict, and reason about data use in programs and types, enabling, for example, parametric quantifiers and linearity to be captured in a dependent setting. We propose<jats:sc>Grtt<\/jats:sc>, study its metatheory, and explore various case studies of its use in reasoning about programs and studying other type theories. We have implemented the theory and highlight the interesting details, including showing an application of grading to optimising the type checking procedure itself.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_17","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"462-490","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Graded Modal Dependent Type Theory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2367-6321","authenticated-orcid":false,"given":"Benjamin","family":"Moon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8474-5971","authenticated-orcid":false,"given":"Harley","family":"Eades III","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A Core Calculus of Dependency. In: POPL. ACM (1999). https:\/\/doi.org\/10.1145\/292540.292555","DOI":"10.1145\/292540.292555"},{"key":"17_CR2","unstructured":"Abel, A.: Resourceful Dependent Types. In: 24th International Conference on Types for Proofs and Programs, Abstracts (2018)"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Abel, A., Bernardy, J.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP), 90:1\u201390:28 (2020). https:\/\/doi.org\/10.1145\/3408972","DOI":"10.1145\/3408972"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Abel, A., Scherer, G.: On irrelevance and algorithmic equality in predicative type theory. Log. Methods Comput. Sci. 8(1) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:29)2012","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Allais, G.: Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0104, pp. 1:1\u20131:22. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2017.1","DOI":"10.4230\/LIPIcs.TYPES.2017.1"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and Semantics of Quantitative Type Theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 56\u201365 (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Atkey, R., Ghani, N., Johann, P.: A relationally parametric model of dependent type theory. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 503\u2013515 (2014). https:\/\/doi.org\/10.1145\/2535838.2535852","DOI":"10.1145\/2535838.2535852"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Bernardy, J.P., Boespflug, M., Newton, R.R., Peyton\u00a0Jones, S., Spiwack, A.: Linear Haskell: practical linearity in a higher-order polymorphic language. Proceedings of the ACM on Programming Languages 2(POPL), \u00a05 (2017). https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: International Workshop on Types for Proofs and Programs. pp. 115\u2013129. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_8","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A Core Quantitative Coeffect Calculus. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08410, pp. 351\u2013370. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys 17(4), 471\u2013523 (Dec 1985). https:\/\/doi.org\/10.1145\/6041.6042","DOI":"10.1145\/6041.6042"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Information and Computation 179(1), 19\u201375 (2002). https:\/\/doi.org\/10.1109\/LICS.1996.561339","DOI":"10.1109\/LICS.1996.561339"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Choudhury, P., Eades\u00a0III, 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","DOI":"10.1145\/3434331"},{"key":"17_CR14","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Ph.D. thesis, INRIA (1986)"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on. pp. 133\u2013142. IEEE (2011). https:\/\/doi.org\/10.1109\/LICS.2011.22","DOI":"10.1109\/LICS.2011.22"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"De\u00a0Amorim, A.A., Gaboardi, M., Gallego\u00a0Arias, E.J., Hsu, J.: Really Natural Linear Indexed Type Checking. In: Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages. p.\u00a05. ACM (2014). https:\/\/doi.org\/10.1145\/2746325.2746335","DOI":"10.1145\/2746325.2746335"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"De\u00a0Vries, E., Plasmeijer, R., Abrahamson, D.M.: Uniqueness typing simplified. In: Symposium on Implementation and Application of Functional Languages. pp. 201\u2013218. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-85373-2_12","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Krishnaswami, N.R.: Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL 3(POPL), 9:1\u20139:28 (2019). https:\/\/doi.org\/10.1145\/3290322","DOI":"10.1145\/3290322"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 281\u2013292. POPL \u201904, ACM, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/964001.964025","DOI":"10.1145\/964001.964025"},{"key":"17_CR21","unstructured":"Eades, H., Stump, A.: Hereditary substitution for Stratified System F. In: International Workshop on Proof-Search in Type Theories, PSTT. vol.\u00a010 (2010)"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: POPL. pp. 357\u2013370 (2013). https:\/\/doi.org\/10.1145\/2429069.2429113","DOI":"10.1145\/2429069.2429113"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Katsumata, S.y., Orchard, D., Breuvart, F., Uustalu, T.: Combining Effects and Coeffects via Grading. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. p. 476\u2013489. ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2951913.2951939","DOI":"10.1145\/2951913.2951939"},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Geuvers, H.: A short and flexible proof of strong normalization for the calculus of constructions. In: Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) Types for Proofs and Programs. pp. 14\u201338. Springer Berlin Heidelberg, Berlin, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60579-7_2","DOI":"10.1007\/3-540-60579-7_2"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: ESOP. pp. 331\u2013350 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Une extension de l\u2019interpretation de g\u00f6del a l\u2019analyse, et son application a l\u2019elimination des coupures dans l\u2019analyse et la theorie destypes. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 63\u201392. Elsevier (1971)","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1\u2013102 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"17_CR28","doi-asserted-by":"publisher","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science 97(1), 1\u201366 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90386-T","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"17_CR29","unstructured":"Girard, J., Taylor, P., Lafont, Y.: Proofs and types, vol.\u00a07. Cambridge University Press Cambridge (1989)"},{"key":"17_CR30","doi-asserted-by":"publisher","unstructured":"Gratzer, D., Sterling, J., Birkedal, L.: Implementing a modal dependent type theory. Proc. ACM Program. Lang. 3(ICFP), 107:1\u2013107:29 (2019). https:\/\/doi.org\/10.1145\/3341711","DOI":"10.1145\/3341711"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Henglein, F., Makholm, H., Niss, H.: Effect types and region-based memory management. Advanced Topics in Types and Programming Languages pp. 87\u2013135 (2005)","DOI":"10.7551\/mitpress\/1104.003.0005"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Hodas, J.S.: Logic programming in intutionistic linear logic: Theory, design and implementation. PhD Thesis, University of Pennsylvania, Department of Computer and Information Science (1994)","DOI":"10.1006\/inco.1994.1036"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. Semantics and logics of computation 14, \u00a079 (1997)","DOI":"10.1017\/CBO9780511526619.004"},{"key":"17_CR34","doi-asserted-by":"publisher","unstructured":"Jiang, J., Eades III, H., de\u00a0Paiva, V.: On the lambek calculus with an exchange modality. In: Ehrhard, T., Fern\u00e1ndez, M., de\u00a0Paiva, V., de\u00a0Falco, L.T. (eds.) Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018. EPTCS, vol.\u00a0292, pp. 43\u201389 (2018). https:\/\/doi.org\/10.4204\/EPTCS.292.4","DOI":"10.4204\/EPTCS.292.4"},{"key":"17_CR35","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proceedings of POPL. pp. 633\u2013646. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"17_CR36","doi-asserted-by":"publisher","unstructured":"Krishnaswami, N.R., Dreyer, D.: Internalizing relational parametricity in the extensional calculus of constructions. In: Computer Science Logic 2013 (CSL2013). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.432","DOI":"10.4230\/LIPIcs.CSL.2013.432"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Pradic, P., Benton, N.: Integrating linear and dependent types. In: ACM SIGPLAN Notices. vol.\u00a050, pp. 17\u201330. ACM (2015)","DOI":"10.1145\/2775051.2676969"},{"key":"17_CR38","doi-asserted-by":"publisher","unstructured":"Leivant, D.: Finitely stratified polymorphism. Information and Computation 93(1), 93\u2013113 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90053-5","DOI":"10.1016\/0890-5401(91)90053-5"},{"key":"17_CR39","unstructured":"Luo, Z., Zhang, Y.: A linear dependent type theory. Types for Proofs and Programs (TYPES 2016), Novi Sad (2016)"},{"key":"17_CR40","doi-asserted-by":"publisher","unstructured":"Martin-L\u00f6f, P.: An Intuitionistic Theory of Types: Predicative Part. In: Rose, H.E., Shepherdson, J.C. (eds.) Studies in Logic and the Foundations of Mathematics, Logic Colloquium \u201973, vol.\u00a080, pp. 73\u2013118. Elsevier (Jan 1975). https:\/\/doi.org\/10.1016\/S0049-237X(08)71945-1","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"17_CR41","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory (Jun 1980)"},{"key":"17_CR42","doi-asserted-by":"publisher","unstructured":"Martin-L\u00f6f, P.: Constructive Mathematics and Computer Programming. In: Cohen, L.J., \u0141o\u015b, J., Pfeiffer, H., Podewski, K.P. (eds.) Studies in Logic and the Foundations of Mathematics, Logic, Methodology and Philosophy of Science VI, vol.\u00a0104, pp. 153\u2013175. Elsevier (Jan 1982). https:\/\/doi.org\/10.1016\/S0049-237X(09)70189-2","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"McBride, C.: I Got Plenty o\u2019 Nuttin\u2019, pp. 207\u2013233. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"17_CR44","unstructured":"Moon, B., Eades III, H., Orchard, D.: Graded modal dependent type theory. CoRR abs\/2010.13163 (2020), https:\/\/arxiv.org\/abs\/2010.13163"},{"key":"17_CR45","doi-asserted-by":"publisher","unstructured":"Nuyts, A., Vezzosi, A., Devriese, D.: Parametric quantifiers for dependent typetheory. Proceedings of the ACM on Programming Languages 1(ICFP), 32:1\u201332:29 (Aug 2017). https:\/\/doi.org\/10.1145\/3110276","DOI":"10.1145\/3110276"},{"key":"17_CR46","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V.B., Eades\u00a0III, H.: Quantitative Program Reasoning with Graded Modal Types. Proc. ACM Program. Lang. 3(ICFP), 110:1\u2013110:30 (Jul 2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"17_CR47","doi-asserted-by":"crossref","unstructured":"Palmgren, E.: On universes in type theory. Twenty-five years of constructive type theory 36, 191\u2013204 (1998)","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"17_CR48","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D., Mycroft, A.: Coeffects: Unified Static Analysis of Context-Dependence. In: ICALP (2). pp. 385\u2013397 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_35","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"17_CR49","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D., Mycroft, A.: Coeffects: A calculus of context-dependent computation. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. pp. 123\u2013135. ICFP \u201914, ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628160","DOI":"10.1145\/2628136.2628160"},{"key":"17_CR50","doi-asserted-by":"publisher","unstructured":"Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. pp. 221\u2013230. IEEE (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932499","DOI":"10.1109\/LICS.2001.932499"},{"key":"17_CR51","doi-asserted-by":"publisher","unstructured":"Reed, J.: Extending higher-order unification to support proof irrelevance. In: International Conference on Theorem Proving in Higher Order Logics. pp. 238\u2013252. Springer (2003). https:\/\/doi.org\/10.1007\/10930755_16","DOI":"10.1007\/10930755_16"},{"key":"17_CR52","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Programming Symposium. pp. 408\u2013425. Springer (1974). https:\/\/doi.org\/10.1007\/3-540-06859-7_148","DOI":"10.1007\/3-540-06859-7_148"},{"key":"17_CR53","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing 83, Proceedings of the IFIP 9th World Computer Congres. pp. 513\u2013523 (1983)"},{"key":"17_CR54","doi-asserted-by":"publisher","unstructured":"Shi, R., Xi, H.: A linear type system for multicore programming in ATS. Science of Computer Programming 78(8), 1176\u20131192 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.09.005","DOI":"10.1016\/j.scico.2012.09.005"},{"key":"17_CR55","doi-asserted-by":"publisher","unstructured":"Tofte, M., Talpin, J.P.: Region-based memory management. Information and computation 132(2), 109\u2013176 (1997). https:\/\/doi.org\/10.1006\/inco.1996.2613","DOI":"10.1006\/inco.1996.2613"},{"key":"17_CR56","doi-asserted-by":"publisher","unstructured":"Tov, J.A., Pucella, R.: Practical affine types. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. pp. 447\u2013458 (2011). https:\/\/doi.org\/10.1145\/1926385.1926436","DOI":"10.1145\/1926385.1926436"},{"key":"17_CR57","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the fourth international conference on Functional programming languages and computer architecture. pp. 347\u2013359 (1989). https:\/\/doi.org\/10.1145\/99370.99404","DOI":"10.1145\/99370.99404"},{"key":"17_CR58","unstructured":"Wadler, P.: Linear Types Can Change the World! In: Programming Concepts and Methods. North (1990)"},{"key":"17_CR59","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Propositions as types. Communications of the ACM 58(12), 75\u201384 (2015). https:\/\/doi.org\/10.1145\/2699407","DOI":"10.1145\/2699407"},{"key":"17_CR60","doi-asserted-by":"crossref","unstructured":"Walker, D.: Substructural type systems. Advanced Topics in Types and Programming Languages pp. 3\u201344 (2005)","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"17_CR61","unstructured":"Wood, J., Atkey, R.: A Linear Algebra Approach to Linear Metatheory. CoRR abs\/2005.02247 (2020), https:\/\/arxiv.org\/abs\/2005.02247"},{"key":"17_CR62","doi-asserted-by":"crossref","unstructured":"Zalakain, U., Dardha, O.: Pi with leftovers: a mechanisation in Agda. arXiv preprint arXiv:2005.05902 (2020)","DOI":"10.1007\/978-3-030-78089-0_9"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T15:35:34Z","timestamp":1724686534000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}