{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:15:32Z","timestamp":1770297332755,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["13156"],"award-info":[{"award-number":["13156"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533359","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks"],"prefix":"10.1145","author":[{"given":"Magnus","family":"Baunsgaard Kristensen","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rasmus Ejlers","family":"Mogelberg","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_3_2_1_3_1","volume-title":"Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a038)","author":"Ahrens Benedikt","year":"2015","unstructured":"Benedikt Ahrens , Paolo Capriotti , and R\u00e9gis Spadotti . 2015 . Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a038) , Thorsten Altenkirch (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17\u201330. https:\/\/doi.org\/10.4230\/LIPIcs.TLCA. 2015.17 10.4230\/LIPIcs.TLCA.2015.17 Benedikt Ahrens, Paolo Capriotti, and R\u00e9gis Spadotti. 2015. Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a038), Thorsten Altenkirch (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17\u201330. https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.17"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500597"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9471-7"},{"key":"e_1_3_2_1_10_1","volume-title":"First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8, 4","author":"Birkedal Lars","year":"2012","unstructured":"Lars Birkedal , Rasmus\u00a0Ejlers M\u00f8gelberg , Jan Schwinghammer , and Kristian St\u00f8vring . 2012. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8, 4 ( 2012 ). Lars Birkedal, Rasmus\u00a0Ejlers M\u00f8gelberg, Jan Schwinghammer, and Kristian St\u00f8vring. 2012. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8, 4 (2012)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129520000080"},{"key":"e_1_3_2_1_13_1","volume-title":"General recursion via coinductive types. Logical Methods in Computer Science 1","author":"Capretta Venanzio","year":"2005","unstructured":"Venanzio Capretta . 2005. General recursion via coinductive types. Logical Methods in Computer Science 1 ( 2005 ). Venanzio Capretta. 2005. General recursion via coinductive types. Logical Methods in Computer Science 1 (2005)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"e_1_3_2_1_15_1","volume-title":"Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020","author":"Cavallo Evan","year":"2020","unstructured":"Evan Cavallo and Robert Harper . 2020 . Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020 , January 13-16, 2020, Barcelona, Spain(LIPIcs, Vol.\u00a0152), Maribel Fern\u00e1ndez and Anca Muscholl (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 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 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain(LIPIcs, Vol.\u00a0152), Maribel Fern\u00e1ndez and Anca Muscholl (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 13:1\u201313:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.13"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000184"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"#cr-split#-e_1_3_2_1_20_1.1","unstructured":"Jesper Cockx. 2020. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0175) Marc Bezem and Assia Mahboubi (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 2:1-2:27. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2019.2 10.4230\/LIPIcs.TYPES.2019.2"},{"key":"#cr-split#-e_1_3_2_1_20_1.2","unstructured":"Jesper Cockx. 2020. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0175) Marc Bezem and Assia Mahboubi (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 2:1-2:27. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2019.2"},{"key":"e_1_3_2_1_21_1","volume-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES","author":"Cohen Cyril","year":"2018","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2018 . Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"#cr-split#-e_1_3_2_1_23_1.1","unstructured":"Thierry Coquand Simon Huber and Christian Sattler. 2019. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0131) Herman Geuvers (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 11:1-11:23. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.11 10.4230\/LIPIcs.FSCD.2019.11"},{"key":"#cr-split#-e_1_3_2_1_23_1.2","unstructured":"Thierry Coquand Simon Huber and Christian Sattler. 2019. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0131) Herman Geuvers (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 11:1-11:23. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.11"},{"key":"e_1_3_2_1_24_1","unstructured":"Thierry Coquand Fabian Ruch and Christian Sattler. 2019. Constructive sheaf models of type theory. Mathematical Structures in Computer Science(2019) 1\u201324.  Thierry Coquand Fabian Ruch and Christian Sattler. 2019. Constructive sheaf models of type theory. Mathematical Structures in Computer Science(2019) 1\u201324."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Nils\u00a0Anders Danielsson. 2010. Beating the Productivity Checker Using Embedded Languages. In PAR Vol.\u00a043. 29\u201348.  Nils\u00a0Anders Danielsson. 2010. Beating the Productivity Checker Using Embedded Languages. In PAR Vol.\u00a043. 29\u201348.","DOI":"10.4204\/EPTCS.43.3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167085"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_2_1_29_1","unstructured":"Martin Hofmann and Thomas Streicher. 1999. Lifting Grothendieck universes. (1999). www.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf Unpublished.  Martin Hofmann and Thomas Streicher. 1999. Lifting Grothendieck universes. (1999). www.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf Unpublished."},{"key":"e_1_3_2_1_30_1","unstructured":"Simon Huber. 2017. A Cubical Type Theory for Higher Inductive Types. (2017). http:\/\/www.cse.chalmers.se\/~simonhu\/misc\/hcomp.pdf  Simon Huber. 2017. A Cubical Type Theory for Higher Inductive Types. (2017). http:\/\/www.cse.chalmers.se\/~simonhu\/misc\/hcomp.pdf"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"J. Hughes L. Pareto and A. Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Papers Presented at the Symposium St. Petersburg Beach Florida USA January 21-24 1996. 410\u2013423.  J. Hughes L. Pareto and A. Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Papers Presented at the Symposium St. Petersburg Beach Florida USA January 21-24 1996. 410\u2013423.","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_1_33_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)."},{"key":"e_1_3_2_1_34_1","unstructured":"R.\u00a0D. Licata I. Orton A.M. Pitts and B. Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0108) H\u00e9l\u00e8ne Kirchner (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik Dagstuhl Germany 22:1\u201322:17.  R.\u00a0D. Licata I. Orton A.M. Pitts and B. Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0108) H\u00e9l\u00e8ne Kirchner (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik Dagstuhl Germany 22:1\u201322:17."},{"key":"e_1_3_2_1_35_1","volume-title":"Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science 16","author":"Mannaa Bassel","year":"2020","unstructured":"Bassel Mannaa , Rasmus\u00a0Ejlers M\u00f8gelberg , and Niccol\u00f2 Veltri . 2020. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science 16 ( 2020 ). Bassel Mannaa, Rasmus\u00a0Ejlers M\u00f8gelberg, and Niccol\u00f2 Veltri. 2020. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science 16 (2020)."},{"key":"e_1_3_2_1_36_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli.  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_38_1","first-page":"1","article-title":"A type theory for productive coprogramming via guarded recursion","volume":"71","author":"M\u00f8gelberg Rasmus\u00a0Ejlers","year":"2014","unstructured":"Rasmus\u00a0Ejlers M\u00f8gelberg . 2014 . A type theory for productive coprogramming via guarded recursion . In CSL-LICS. 71 : 1 \u2013 71 :10. Rasmus\u00a0Ejlers M\u00f8gelberg. 2014. A type theory for productive coprogramming via guarded recursion. In CSL-LICS. 71:1\u201371:10.","journal-title":"CSL-LICS."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000087"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290317"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.351.13"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_1_43_1","unstructured":"I. Orton and A.M. Pitts. 2018. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science Volume 14 Issue 4 (Dec 2018).  I. Orton and A.M. Pitts. 2018. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science Volume 14 Issue 4 (Dec 2018)."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.020"},{"key":"e_1_3_2_1_45_1","volume-title":"Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013","author":"Sacchini Jorge\u00a0Luis","year":"2013","unstructured":"Jorge\u00a0Luis Sacchini . 2013 . Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013 , New Orleans, LA, USA , June 25-28, 2013. 233\u2013242. Jorge\u00a0Luis Sacchini. 2013. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. 233\u2013242."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676983"},{"key":"e_1_3_2_1_47_1","volume-title":"Normalization for Cubical Type Theory. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021","author":"Sterling Jonathan","year":"2021","unstructured":"Jonathan Sterling and Carlo Angiuli . 2021 . Normalization for Cubical Type Theory. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021 , Rome, Italy, June 29 - July 2, 2021. IEEE, 1\u201315. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470719 10.1109\/LICS52264.2021.9470719 Jonathan Sterling and Carlo Angiuli. 2021. Normalization for Cubical Type Theory. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1\u201315. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_1_48_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 , Institute for Advanced Study. The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Institute for Advanced Study."},{"key":"e_1_3_2_1_49_1","volume-title":"6th International Conference on Formal Structures for Computation and Deduction, FSCD","author":"Veltri Niccol\u00f2","year":"2021","unstructured":"Niccol\u00f2 Veltri . 2021. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor . In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 , July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)(LIPIcs, Vol.\u00a0195), Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 22:1\u201322:18. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.22 10.4230\/LIPIcs.FSCD.2021.22 Niccol\u00f2 Veltri. 2021. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)(LIPIcs, Vol.\u00a0195), Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 22:1\u201322:18. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.22"},{"key":"e_1_3_2_1_50_1","volume-title":"4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019","author":"Veltri Niccol\u00f2","year":"2019","unstructured":"Niccol\u00f2 Veltri and Niels van\u00a0der Weide . 2019 . Guarded Recursion in Agda via Sized Types . In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 , June 24-30, 2019, Dortmund, Germany(LIPIcs, Vol.\u00a0131), Herman Geuvers (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 32:1\u201332:19. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2019.32 10.4230\/LIPIcs.FSCD.2019.32 Niccol\u00f2 Veltri and Niels van\u00a0der Weide. 2019. Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany(LIPIcs, Vol.\u00a0131), Herman Geuvers (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 32:1\u201332:19. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.32"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373814"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.009"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533359","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533359","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:10Z","timestamp":1750186930000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533359"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":55,"alternative-id":["10.1145\/3531130.3533359","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533359","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}