{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:50Z","timestamp":1767929630810,"version":"3.49.0"},"reference-count":133,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2021,10,5]],"date-time":"2021-10-05T00:00:00Z","timestamp":1633392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["MURI FA9550-15-1-0053 and FA9550-19-1-0216"],"award-info":[{"award-number":["MURI FA9550-15-1-0053 and FA9550-19-1-0216"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2021,12,31]]},"abstract":"<jats:p>\n            The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design:\n            <jats:italic>the phase distinction<\/jats:italic>\n            ,\n            <jats:italic>computational effects<\/jats:italic>\n            , and\n            <jats:italic>type abstraction<\/jats:italic>\n            . We contribute a fresh \u201csynthetic\u201d take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a\n            <jats:italic>lax modality<\/jats:italic>\n            that encapsulates computational effects, placing\n            <jats:italic>projectibility<\/jats:italic>\n            of module expressions on a type-theoretic basis.\n          <\/jats:p>\n          <jats:p>\n            Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a\n            <jats:italic>parametricity structure<\/jats:italic>\n            . Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-\n            <jats:italic>relevant<\/jats:italic>\n            families, where there may be non-trivial evidence witnessing the relatedness of two programs\u2014simplifying the metatheory of strong sums over the collection of types, for although there can be no \u201crelation classifying relations,\u201d one easily accommodates a \u201cfamily classifying small families.\u201d\n          <\/jats:p>\n          <jats:p>\n            Using the insight that logical relations\/parametricity is\n            <jats:italic>itself<\/jats:italic>\n            a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan\n            <jats:italic>logical relations as types<\/jats:italic>\n            , by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic\n            <jats:italic>Artin gluing<\/jats:italic>\n            construction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.\n          <\/jats:p>\n          <jats:p\/>","DOI":"10.1145\/3474834","type":"journal-article","created":{"date-parts":[[2021,10,5]],"date-time":"2021-10-05T20:01:15Z","timestamp":1633464075000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Logical Relations as Types: Proof-Relevant Parametricity for Program Modules"],"prefix":"10.1145","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0585-5564","authenticated-orcid":false,"given":"Jonathan","family":"Sterling","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9400-2941","authenticated-orcid":false,"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90082-5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_3"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS\u201987)","author":"Allen Stuart Frazier","year":"1987","unstructured":"Stuart Frazier Allen . 1987 . A non-type-theoretic definition of martin-l\u00f6f\u2019s types . In Proceedings of the Symposium on Logic in Computer Science (LICS\u201987) . IEEE, 215\u2013221. Stuart Frazier Allen. 1987. A non-type-theoretic definition of martin-l\u00f6f\u2019s types. In Proceedings of the Symposium on Logic in Computer Science (LICS\u201987). IEEE, 215\u2013221."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/648334.755596"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916)","volume":"52","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch and Ambrus Kaposi . 2016 . Normalisation by evaluation for dependent types . In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916) , Leibniz International Proceedings in Informatics , Vol. 52 , Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1\u20136:16. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.6 10.4230\/LIPIcs.FSCD.2016.6 Thorsten Altenkirch and Ambrus Kaposi. 2016. Normalisation by evaluation for dependent types. In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916), Leibniz International Proceedings in Informatics, Vol. 52, Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1\u20136:16. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_2_1_7_1","volume-title":"New Spaces in Mathematics: Formal and Conceptual Reflections, Mathieu Anel and Gabriel Catren (Eds.).","author":"Anel Mathieu","unstructured":"Mathieu Anel and Andr\u00e9 Joyal . 2021. Topo-logie . In New Spaces in Mathematics: Formal and Conceptual Reflections, Mathieu Anel and Gabriel Catren (Eds.). Vol. 1 . Cambridge University Press , 155\u2013257. https:\/\/doi.org\/10.1017\/9781108854429.007 10.1017\/9781108854429.007 Mathieu Anel and Andr\u00e9 Joyal. 2021. Topo-logie. In New Spaces in Mathematics: Formal and Conceptual Reflections, Mathieu Anel and Gabriel Catren (Eds.). Vol. 1. Cambridge University Press, 155\u2013257. https:\/\/doi.org\/10.1017\/9781108854429.007"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_2_1_10_1","volume-title":"Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas","author":"Artin Michael","year":"1963","unstructured":"Michael Artin , Alexander Grothendieck , and Jean-Louis Verdier . 1972. Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas . Springer-Verlag , Berlin . S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois-Marie 1963 \u20131964 (SGA 4), Dirig\u00e9 par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat, Lecture Notes in Mathematics, Vol. 269, 270, 305. Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. 1972. Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas. Springer-Verlag, Berlin. S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois-Marie 1963\u20131964 (SGA 4), Dirig\u00e9 par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat, Lecture Notes in Mathematics, Vol. 269, 270, 305."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647844.760807"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 21st EACSL Annual Conference\/26th International Workshop on Computer Science Logic, Leibniz International Proceedings in Informatics","volume":"16","author":"Atkey Robert","year":"2012","unstructured":"Robert Atkey . 2012 . Relational parametricity for higher kinds . In Proceedings of the 21st EACSL Annual Conference\/26th International Workshop on Computer Science Logic, Leibniz International Proceedings in Informatics , Vol. 16 . Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, 46\u201361. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2012.46 10.4230\/LIPIcs.CSL.2012.46 Robert Atkey. 2012. Relational parametricity for higher kinds. In Proceedings of the 21st EACSL Annual Conference\/26th International Workshop on Computer Science Logic, Leibniz International Proceedings in Informatics, Vol. 16. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, 46\u201361. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.46"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535852"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/nkt030"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Nick Benton Martin Hofmann and Vivek Nigam. 2013. Proof-relevant logical relations for name generation. In Typed Lambda Calculi and Applications Masahito Hasegawa (Ed.). Springer Berlin 48\u201360.   Nick Benton Martin Hofmann and Vivek Nigam. 2013. Proof-relevant logical relations for name generation. In Typed Lambda Calculi and Applications Masahito Hasegawa (Ed.). Springer Berlin 48\u201360.","DOI":"10.1007\/978-3-642-38946-7_6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535869"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2012.02.039"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500577"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/182590.182431"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916), Leibniz International Proceedings in Informatics","volume":"62","author":"Birkedal Lars","year":"2016","unstructured":"Lars Birkedal , Ale\u0161 Bizjak , Ranald Clouston , Hans Bugge Grathwohl , Bas Spitters , and Andrea Vezzosi . 2016 . Guarded cubical type theory: Path equality for guarded recursion . In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916), Leibniz International Proceedings in Informatics , Vol. 62 , Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 23:1\u201323:17. Lars Birkedal, Ale\u0161 Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2016. Guarded cubical type theory: Path equality for guarded recursion. In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916), Leibniz International Proceedings in Informatics, Vol. 62, Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 23:1\u201323:17."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004834"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_1_26_1","unstructured":"Edwin Brady. 2021. Idris 2: Quantitative Type Theory in PracticearXiv:2104.00480 [cs.PL]. Retrieved from https:\/\/arxiv.org\/abs\/ [cs.PL].  Edwin Brady. 2021. Idris 2: Quantitative Type Theory in PracticearXiv:2104.00480 [cs.PL]. Retrieved from https:\/\/arxiv.org\/abs\/ [cs.PL]."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004080"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North-Holland, 479\u2013504","author":"Cardelli Luca","year":"1990","unstructured":"Luca Cardelli and Xavier Leroy . 1990 . Abstract types and the dot notation . In Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North-Holland, 479\u2013504 . Luca Cardelli and Xavier Leroy. 1990. Abstract types and the dot notation. In Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North-Holland, 479\u2013504."},{"key":"e_1_2_1_30_1","volume-title":"Undecidability of equality in the free locally cartesian closed category (extended version). Log. Methods Comput. Sci. 13, 4","author":"Castellan Simon","year":"2017","unstructured":"Simon Castellan , Pierre Clairambault , and Peter Dybjer . 2017. Undecidability of equality in the free locally cartesian closed category (extended version). Log. Methods Comput. Sci. 13, 4 ( 2017 ). Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2017. Undecidability of equality in the free locally cartesian closed category (extended version). Log. Methods Comput. Sci. 13, 4 (2017)."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920), Leibniz International Proceedings in Informatics","volume":"152","author":"Cavallo Evan","year":"2020","unstructured":"Evan Cavallo and Robert Harper . 2020 . Internal parametricity for cubical type theory . In Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920), Leibniz International Proceedings in Informatics , Vol. 152 , Maribel Fern\u00e1ndez and Anca Muscholl (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 13:1\u201313:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2020.13 10.4230\/LIPIcs.CSL.2020.13 Evan Cavallo and Robert Harper. 2020. Internal parametricity for cubical type theory. In Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920), Leibniz International Proceedings in Informatics, Vol. 152, Maribel Fern\u00e1ndez and Anca Muscholl (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 13:1\u201313:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.13"},{"key":"e_1_2_1_33_1","volume-title":"Andrew M. Pitts, and Bas Spitters.","author":"Clouston Ranald","year":"2018","unstructured":"Ranald Clouston , Bassel Mannaa , Rasmus Ejlers M\u00f8gelberg , Andrew M. Pitts, and Bas Spitters. 2018 . Modal Dependent Type Theory and Dependent Right Adjoints. Retrieved from arXiv:1804.05236. Retrieved fromhttps:\/\/arxiv.org\/abs\/1804.05236. Ranald Clouston, Bassel Mannaa, Rasmus Ejlers M\u00f8gelberg, Andrew M. Pitts, and Bas Spitters. 2018. Modal Dependent Type Theory and Dependent Right Adjoints. Retrieved from arXiv:1804.05236. Retrieved fromhttps:\/\/arxiv.org\/abs\/1804.05236."},{"key":"e_1_2_1_34_1","first-page":"10","article-title":"Cubical type theory: A constructive interpretation of the univalence axiom","volume":"4","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2017 . Cubical type theory: A constructive interpretation of the univalence axiom . IfCoLog J. Log. Appl. 4 , 10 (Nov. 2017), 3127\u20133169. http:\/\/www.collegepublications.co.uk\/journals\/ifcolog\/?00019. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2017. Cubical type theory: A constructive interpretation of the univalence axiom. IfCoLog J. Log. Appl. 4, 10 (Nov. 2017), 3127\u20133169. http:\/\/www.collegepublications.co.uk\/journals\/ifcolog\/?00019.","journal-title":"IfCoLog J. Log. Appl."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/10510"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)","volume":"131","author":"Coquand Thierry","year":"2019","unstructured":"Thierry Coquand , Simon Huber , and Christian Sattler . 2019 . Homotopy canonicity for cubical type theory . In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919) Leibniz International Proceedings in Informatics , Vol. 131 , Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. Thierry Coquand, Simon Huber, and Christian Sattler. 2019. Homotopy canonicity for cubical type theory. In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)Leibniz International Proceedings in Informatics, Vol. 131, Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009892"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290323"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000222"},{"key":"e_1_2_1_41_1","unstructured":"Karl Crary and Robert Harper. 2009. Mechanized Definition of Standard ML (alpha release). Retrieved from https:\/\/www.cs.cmu.edu\/ crary\/papers\/2009\/mldef-alpha.tar.gz.  Karl Crary and Robert Harper. 2009. Mechanized Definition of Standard ML (alpha release). Retrieved from https:\/\/www.cs.cmu.edu\/ crary\/papers\/2009\/mldef-alpha.tar.gz."},{"key":"e_1_2_1_42_1","unstructured":"Leonardo De Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language (System Description) (unpublished).   Leonardo De Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language (System Description) (unpublished)."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(75)90015-8"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291220.1291196"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604151"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190229"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(96)00164-8"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/277652.277730"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"e_1_2_1_55_1","unstructured":"Daniel Gratzer. 2021. Normalization for multimodal type theory. arXiv:2106.01414[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2106.01414 [cs.LO].  Daniel Gratzer. 2021. Normalization for multimodal type theory. arXiv:2106.01414[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2106.01414 [cs.LO]."},{"key":"e_1_2_1_56_1","unstructured":"Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: Sketching and adequacy. arXiv:2012.10783[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2012.10783 [cs.LO].  Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: Sketching and adequacy. arXiv:2012.10783[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2012.10783 [cs.LO]."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/3002812"},{"key":"e_1_2_1_59_1","unstructured":"Robert Harper. 2019. PFPL Supplement: How to (Re)Invent Tait\u2019s Method. Retrieved from http:\/\/www.cs.cmu.edu\/ rwh\/pfpl\/supplements\/tait.pdf.  Robert Harper. 2019. PFPL Supplement: How to (Re)Invent Tait\u2019s Method. Retrieved from http:\/\/www.cs.cmu.edu\/ rwh\/pfpl\/supplements\/tait.pdf."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/345868.345906"},{"key":"e_1_2_1_65_1","volume-title":"Semantics and Logics of Computation","author":"Hofmann Martin","unstructured":"Martin Hofmann . 1997. Syntax and semantics of dependent types . In Semantics and Logics of Computation . Cambridge University Press , 79\u2013130. Martin Hofmann. 1997. Syntax and semantics of dependent types. In Semantics and Logics of Computation. Cambridge University Press, 79\u2013130."},{"key":"e_1_2_1_66_1","unstructured":"Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Retrieved from https:\/\/www2.mathematik.tu-darmstadt.de\/ streicher\/NOTES\/lift.pdf.  Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Retrieved from https:\/\/www2.mathematik.tu-darmstadt.de\/ streicher\/NOTES\/lift.pdf."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"e_1_2_1_68_1","volume-title":"First steps in synthetic domain theory","author":"Hyland J. M. E.","unstructured":"J. M. E. Hyland . 1991. First steps in synthetic domain theory . In Category Theory, Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini (Eds.). Springer , Berlin , 131\u2013156. J. M. E. Hyland. 1991. First steps in synthetic domain theory. In Category Theory, Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini (Eds.). Springer, Berlin, 131\u2013156."},{"key":"e_1_2_1_69_1","volume-title":"Topos Theory","author":"Johnstone Peter","unstructured":"Peter Johnstone . 1977. Topos Theory . Academic Press . Peter Johnstone. 1977. Topos Theory. Academic Press."},{"key":"e_1_2_1_70_1","volume-title":"Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. Number 43 in Oxford Logical Guides","author":"Johnstone Peter T.","unstructured":"Peter T. Johnstone . 2002. Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. Number 43 in Oxford Logical Guides . Oxford Science Publications . Peter T. Johnstone. 2002. Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. Number 43 in Oxford Logical Guides. Oxford Science Publications."},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)","volume":"131","author":"Kaposi Ambrus","year":"2019","unstructured":"Ambrus Kaposi , Simon Huber , and Christian Sattler . 2019 . Gluing for type theory . In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919) Leibniz International Proceedings in Informatics , Vol. 131 , Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. Ambrus Kaposi, Simon Huber, and Christian Sattler. 2019. Gluing for type theory. In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)Leibniz International Proceedings in Informatics, Vol. 131, Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany."},{"key":"e_1_2_1_72_1","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Kripke Saul A.","unstructured":"Saul A. Kripke . 1965. Semantical analysis of intuitionistic logic I . In Formal Systems and Recursive Functions, J. N. Crossley and M. A. E. Dummett (Eds.). Studies in Logic and the Foundations of Mathematics , Vol. 40 . Elsevier , 92\u2013130. https:\/\/doi.org\/10.1016\/S0049-237X(08)71685-9 10.1016\/S0049-237X(08)71685-9 Saul A. Kripke. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions, J. N. Crossley and M. A. E. Dummett (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 40. Elsevier, 92\u2013130. https:\/\/doi.org\/10.1016\/S0049-237X(08)71685-9"},{"key":"e_1_2_1_73_1","volume-title":"Proceedings of the Computer Science Logic 2013 (CSL\u201913)Leibniz International Proceedings in Informatics","volume":"451","author":"Neelakantan","year":"2013","unstructured":"Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing relational parametricity in the extensional calculus of constructions . In Proceedings of the Computer Science Logic 2013 (CSL\u201913)Leibniz International Proceedings in Informatics , Vol. 23), Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 432\u2013 451 . https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2013 .432 10.4230\/LIPIcs.CSL.2013.432 Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing relational parametricity in the extensional calculus of constructions. In Proceedings of the Computer Science Logic 2013 (CSL\u201913)Leibniz International Proceedings in Informatics, Vol. 23), Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 432\u2013451. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.432"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199476"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001933"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"e_1_2_1_80_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml System Manual. https:\/\/opam.ocaml.org\/packages\/ocaml-manual\/.  Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml System Manual. https:\/\/opam.ocaml.org\/packages\/ocaml-manual\/."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.5555\/984044"},{"key":"e_1_2_1_82_1","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane and Ieke Moerdijk . 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory . Springer , New York . Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386336"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_1_85_1","unstructured":"Per Martin-L\u00f6f. 2013. Invariance under isomorphism and definability. Presented in the Ernest Nagel Lectures in Philosophy & Science at Carnegie Mellon University.  Per Martin-L\u00f6f. 2013. Invariance under isomorphism and definability. Presented in the Ernest Nagel Lectures in Philosophy & Science at Carnegie Mellon University."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.5555\/645722.666541"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969038"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676970"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.5555\/575336"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73563"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.40"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.5555\/648332.755571"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.5555\/92094"},{"key":"e_1_2_1_98_1","unstructured":"Andreas Nuyts. 2018. Presheaf models of relational modalities in dependent type theory. arXiv:1805.08684. Retrieved fromhttps:\/\/arxiv.org\/abs\/1805.08684.  Andreas Nuyts. 2018. Presheaf models of relational modalities in dependent type theory. arXiv:1805.08684. Retrieved fromhttps:\/\/arxiv.org\/abs\/1805.08684."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.5555\/22584.24310"},{"key":"e_1_2_1_101_1","volume-title":"Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916)Leibniz International Proceedings in Informatics","volume":"62","author":"Orton Ian","year":"2016","unstructured":"Ian Orton and Andrew M. Pitts . 2016. Axioms for modelling cubical type theory in a topos . In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916)Leibniz International Proceedings in Informatics , Vol. 62 , Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 24:1\u201324:19. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2016 .24 10.4230\/LIPIcs.CSL.2016.24 Ian Orton and Andrew M. Pitts. 2016. Axioms for modelling cubical type theory in a topos. In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916)Leibniz International Proceedings in Informatics, Vol. 62, Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 24:1\u201324:19. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.24"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.5555\/648331.755423"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671433"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_2_1_109_1","unstructured":"The RedPRL Development Team. 2018. rgb].91 .31 .27redtt. Retrieved from https:\/\/www.github.com\/RedPRL\/redtt.  The RedPRL Development Team. 2018. rgb].91 .31 .27redtt. Retrieved from https:\/\/www.github.com\/RedPRL\/redtt."},{"key":"e_1_2_1_110_1","unstructured":"The RedPRL Development Team. 2020. rgb].012 .27 .46cooltt. Retreived from https:\/\/www.github.com\/RedPRL\/cooltt.  The RedPRL Development Team. 2020. rgb].012 .27 .46cooltt. Retreived from https:\/\/www.github.com\/RedPRL\/cooltt."},{"key":"e_1_2_1_111_1","unstructured":"John C. Reynolds. 1983. Types abstraction and parametric polymorphism. In Information Processing.  John C. Reynolds. 1983. Types abstraction and parametric polymorphism. In Information Processing."},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199452"},{"key":"e_1_2_1_113_1","doi-asserted-by":"crossref","first-page":"147","DOI":"10.21136\/HS.2017.06","article-title":"A type theory for synthetic -categories","volume":"1","author":"Riehl Emily","year":"2017","unstructured":"Emily Riehl and Michael Shulman . 2017 . A type theory for synthetic -categories . High. Struct. 1 (2017), 147 \u2013 224 . Issue 1. https:\/\/journals.mq.edu.au\/index.php\/higher_structures\/article\/view\/36. Emily Riehl and Michael Shulman. 2017. A type theory for synthetic -categories. High. Struct. 1 (2017), 147\u2013224. Issue 1. https:\/\/journals.mq.edu.au\/index.php\/higher_structures\/article\/view\/36.","journal-title":"High. Struct."},{"key":"e_1_2_1_114_1","first-page":"1","article-title":"Modalities in homotopy type theory","volume":"16","author":"Rijke Egbert","year":"2020","unstructured":"Egbert Rijke , Michael Shulman , and Bas Spitters . 2020 . Modalities in homotopy type theory . Log. Methods Comput. Sci. 16 , 1 (Jan. 2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:2)2020 10.23638\/LMCS-16(1:2)2020 Egbert Rijke, Michael Shulman, and Bas Spitters. 2020. Modalities in homotopy type theory. Log. Methods Comput. Sci. 16, 1 (Jan. 2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:2)2020","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_2_1_115_1","volume-title":"Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 364\u2013371","author":"Robinson E.","year":"1994","unstructured":"E. Robinson and G. Rosolini . 1994. Reflexive graphs and parametric polymorphism . In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 364\u2013371 . https:\/\/doi.org\/10.1109\/LICS. 1994 .316053 10.1109\/LICS.1994.316053 E. Robinson and G. Rosolini. 1994. Reflexive graphs and parametric polymorphism. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 364\u2013371. https:\/\/doi.org\/10.1109\/LICS.1994.316053"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000205"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1145\/317765.317801"},{"key":"e_1_2_1_119_1","unstructured":"Michael Shulman. 2013. Scones Logical Relations and Parametricity. Retrieved from https:\/\/golem.ph.utexas.edu\/category\/2013\/04\/scones_logical_relations_and_p.html.  Michael Shulman. 2013. Scones Logical Relations and Parametricity. Retrieved from https:\/\/golem.ph.utexas.edu\/category\/2013\/04\/scones_logical_relations_and_p.html."},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209141"},{"key":"e_1_2_1_122_1","unstructured":"The Stacks Project Authors. 2017. Stacks Project. Retrieved from http:\/\/stacks.math.columbia.edu.  The Stacks Project Authors. 2017. Stacks Project. Retrieved from http:\/\/stacks.math.columbia.edu."},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591370.2591394"},{"key":"e_1_2_1_124_1","unstructured":"Jonathan Sterling and Carlo Angiuli. 2020. Gluing models of type theory along flat functors (unpublished).   Jonathan Sterling and Carlo Angiuli. 2020. Gluing models of type theory along flat functors (unpublished)."},{"key":"e_1_2_1_125_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_2_1_126_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)","volume":"131","author":"Sterling Jonathan","year":"2019","unstructured":"Jonathan Sterling , Carlo Angiuli , and Daniel Gratzer . 2019 . Cubical syntax for reflection-free extensional equality . In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919) Leibniz International Proceedings in Informatics , Vol. 131 , Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1\u201331:25. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31 10.4230\/LIPIcs.FSCD.2019.31 Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019. Cubical syntax for reflection-free extensional equality. In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)Leibniz International Proceedings in Informatics, Vol. 131, Herman Geuvers (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1\u201331:25. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_2_1_127_1","volume-title":"Carlo Angiuli, and Daniel Gratzer","author":"Sterling Jonathan","year":"2020","unstructured":"Jonathan Sterling , Carlo Angiuli, and Daniel Gratzer . 2020 . A cubical language for Bishop sets. (2020). arXiv:2003.01491[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2003.01491 [cs.LO]. Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2020. A cubical language for Bishop sets. (2020). arXiv:2003.01491[cs.LO]. Retrieved from https:\/\/arxiv.org\/abs\/2003.01491 [cs.LO]."},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325724"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.5555\/121358"},{"key":"e_1_2_1_133_1","volume-title":"From Sets and Types to Topology and Analysis: Towards Practical Foundations for Constructive Mathematics","author":"Streicher Thomas","year":"1985","unstructured":"Thomas Streicher . 2005. Universes in toposes . In From Sets and Types to Topology and Analysis: Towards Practical Foundations for Constructive Mathematics , Oxford Logical Guides, Vol. 48 , Laura Crosilla and Peter Schuster (Eds.). Oxford University Press , Oxford, 78\u201390. https:\/\/doi.org\/10.1093\/acprof:oso\/9780 1985 66519.001.0001 10.1093\/acprof:oso Thomas Streicher. 2005. Universes in toposes. In From Sets and Types to Topology and Analysis: Towards Practical Foundations for Constructive Mathematics, Oxford Logical Guides, Vol. 48, Laura Crosilla and Peter Schuster (Eds.). Oxford University Press, Oxford, 78\u201390. https:\/\/doi.org\/10.1093\/acprof:oso\/9780198566519.001.0001"},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159883"},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_137_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_2_1_138_1","volume-title":"Locales and Toposes as Spaces","author":"Vickers Steven","unstructured":"Steven Vickers . 2007. Locales and Toposes as Spaces . Springer Netherlands , Dordrecht , 429\u2013496. https:\/\/doi.org\/10.1007\/978-1-4020-5587-4_8 10.1007\/978-1-4020-5587-4_8 Steven Vickers. 2007. Locales and Toposes as Spaces. Springer Netherlands, Dordrecht, 429\u2013496. https:\/\/doi.org\/10.1007\/978-1-4020-5587-4_8"},{"key":"e_1_2_1_139_1","unstructured":"Vladimir Voevodsky. 2006. A very short note on homotopy -calculus. Retrieved from http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf.  Vladimir Voevodsky. 2006. A very short note on homotopy -calculus. Retrieved from http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf."},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.042"},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159877"},{"key":"e_1_2_1_144_1","volume-title":"Lectures on elementary topoi","author":"Wraith G. C.","unstructured":"G. C. Wraith . 1975. Lectures on elementary topoi . In Model Theory and Topoi, F. William Lawvere, Christian Maurer, and Gavin C. Wraith (Eds.). Springer , Berlin . G. C. Wraith. 1975. Lectures on elementary topoi. In Model Theory and Topoi, F. William Lawvere, Christian Maurer, and Gavin C. Wraith (Eds.). Springer, Berlin."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3474834","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3474834","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3474834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:44Z","timestamp":1750195724000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3474834"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,5]]},"references-count":133,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12,31]]}},"alternative-id":["10.1145\/3474834"],"URL":"https:\/\/doi.org\/10.1145\/3474834","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,5]]},"assertion":[{"value":"2020-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-10-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}