{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:54Z","timestamp":1767929574318,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":41,"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":["25804"],"award-info":[{"award-number":["25804"]}],"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.3532398","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":16,"title":["Normalization for Multimodal Type Theory"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[\n  1\n  ]  Andreas Abel.2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation.  [1] Andreas Abel.2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation."},{"key":"e_1_3_2_1_2_1","volume-title":"A non-type-theoretic semantics for type-theoretic language. Ph.\u00a0D. Dissertation","author":"Allen Stuart\u00a0Frazier","unstructured":"Stuart\u00a0Frazier Allen . 1987. A non-type-theoretic semantics for type-theoretic language. Ph.\u00a0D. Dissertation . Cornell University . Stuart\u00a0Frazier Allen. 1987. A non-type-theoretic semantics for type-theoretic language. Ph.\u00a0D. Dissertation. Cornell University."},{"key":"e_1_3_2_1_3_1","volume-title":"Category Theory and Computer Science (Berlin","author":"Altenkirch Thorsten","unstructured":"Thorsten Altenkirch , Martin Hofmann , and Thomas Streicher . 1995. Categorical reconstruction of a reduction free normalization proof . In Category Theory and Computer Science (Berlin , Heidelberg ), David Pitt, David\u00a0E. Rydeheard, and Peter Johnstone (Eds.). Springer Berlin Heidelberg , 182\u2013199. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science (Berlin, Heidelberg), David Pitt, David\u00a0E. Rydeheard, and Peter Johnstone (Eds.). Springer Berlin Heidelberg, 182\u2013199."},{"key":"e_1_3_2_1_4_1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a052)","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch and Ambrus Kaposi . 2016 . Normalisation by Evaluation for Dependent Types . In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a052) , 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 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a052), 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_3_2_1_5_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 . 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. 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_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_1_7_1","volume-title":"Guarded Cubical Type Theory. Journal of Automated Reasoning63","author":"Birkedal Lars","year":"2019","unstructured":"Lars Birkedal , Ale\u0161 Bizjak , Ranald Clouston , Hans\u00a0Bugge Grathwohl , Bas Spitters , and Andrea Vezzosi . 2019. Guarded Cubical Type Theory. Journal of Automated Reasoning63 ( 2019 ), 211\u2013253. Lars Birkedal, Ale\u0161 Bizjak, Ranald Clouston, Hans\u00a0Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2019. Guarded Cubical Type Theory. Journal of Automated Reasoning63 (2019), 211\u2013253."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_1_9_1","unstructured":"Rafa\u00ebl Bocquet Ambrus Kaposi and Christian Sattler. 2021. Induction principles for type theories internally to presheaf categories. arxiv:2102.11649\u00a0[cs.LO]  Rafa\u00ebl Bocquet Ambrus Kaposi and Christian Sattler. 2021. Induction principles for type theories internally to presheaf categories. arxiv:2102.11649\u00a0[cs.LO]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001183"},{"key":"e_1_3_2_1_11_1","volume-title":"Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal\u00a0Lago (Eds.)","author":"Clouston Ranald","unstructured":"Ranald Clouston . 2018. Fitch-Style Modal Lambda Calculi . In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal\u00a0Lago (Eds.) . Springer International Publishing , 258\u2013275. Ranald Clouston. 2018. Fitch-Style Modal Lambda Calculi. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal\u00a0Lago (Eds.). Springer International Publishing, 258\u2013275."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_14_1","unstructured":"Daniel Gratzer. 2021. Normalization for multimodal type theory. arxiv:2106.01414\u00a0[cs.LO]  Daniel Gratzer. 2021. Normalization for multimodal type theory. arxiv:2106.01414\u00a0[cs.LO]"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_2_1_16_1","volume-title":"Multimodal Dependent Type Theory. Logical Methods in Computer Science","author":"Gratzer Daniel","year":"2021","unstructured":"Daniel Gratzer , G.\u00a0 A. Kavvos , Andreas Nuyts , and Lars Birkedal . 2021. Multimodal Dependent Type Theory. Logical Methods in Computer Science Volume 17 , Issue 3 ( July 2021 ). https:\/\/doi.org\/10.46298\/lmcs-17(3:11)2021 10.46298\/lmcs-17(3:11)2021 Daniel Gratzer, G.\u00a0A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021. Multimodal Dependent Type Theory. Logical Methods in Computer Science Volume 17, Issue 3 (July 2021). https:\/\/doi.org\/10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_1_17_1","unstructured":"Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. arxiv:2012.10783\u00a0[cs.LO]  Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. arxiv:2012.10783\u00a0[cs.LO]"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_2_1_20_1","volume-title":"Semantics and Logics of Computation, Andrew\u00a0M. Pitts and P.\u00a0Dybjer (Eds.)","author":"Hofmann Martin","unstructured":"Martin Hofmann . 1997. Syntax and Semantics of Dependent Types . In Semantics and Logics of Computation, Andrew\u00a0M. Pitts and P.\u00a0Dybjer (Eds.) . Cambridge University Press , 79\u2013130. https:\/\/doi.org\/10.1017\/CBO9780511526619.004 10.1017\/CBO9780511526619.004 Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation, Andrew\u00a0M. Pitts and P.\u00a0Dybjer (Eds.). Cambridge University Press, 79\u2013130. https:\/\/doi.org\/10.1017\/CBO9780511526619.004"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788940"},{"key":"e_1_3_2_1_22_1","unstructured":"Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. (1997). https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf Unpublished note.  Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. (1997). https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf Unpublished note."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD","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 2019), Herman Geuvers (Ed.). Vol.\u00a0131. 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 2019), Herman Geuvers (Ed.). Vol.\u00a0131."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(98)00114-5"},{"key":"e_1_3_2_1_26_1","volume-title":"2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a084)","author":"Licata R.","year":"2017","unstructured":"Daniel\u00a0 R. Licata , Michael Shulman , and Mitchell Riley . 2017 . A Fibrational Framework for Substructural and Modal Logics . In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a084) , Dale Miller (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 25:1\u201325:22. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2017.25 10.4230\/LIPIcs.FSCD.2017.25 Daniel\u00a0R. Licata, Michael Shulman, and Mitchell Riley. 2017. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a084), Dale Miller (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 25:1\u201325:22. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.25"},{"key":"e_1_3_2_1_27_1","unstructured":"Per Martin-L\u00f6f. 1992. Substitution calculus. Notes from a lecture given in G\u00f6teborg.  Per Martin-L\u00f6f. 1992. Substitution calculus. Notes from a lecture given in G\u00f6teborg."},{"key":"e_1_3_2_1_28_1","volume-title":"Mitchell and Andre Scedrov","author":"C.","year":"1993","unstructured":"John\u00a0 C. Mitchell and Andre Scedrov . 1993 . Notes on sconing and relators. In Computer Science Logic, E.\u00a0B\u00f6rger, G.\u00a0J\u00e4ger, H.\u00a0Kleine\u00a0B\u00fcning, S.\u00a0Martini, and M.\u00a0M. Richter (Eds.). Springer Berlin Heidelberg , 352\u2013378. https:\/\/doi.org\/10.1007\/3-540-56992-8_21 10.1007\/3-540-56992-8_21 John\u00a0C. Mitchell and Andre Scedrov. 1993. Notes on sconing and relators. In Computer Science Logic, E.\u00a0B\u00f6rger, G.\u00a0J\u00e4ger, H.\u00a0Kleine\u00a0B\u00fcning, S.\u00a0Martini, and M.\u00a0M. Richter (Eds.). Springer Berlin Heidelberg, 352\u2013378. https:\/\/doi.org\/10.1007\/3-540-56992-8_21"},{"key":"e_1_3_2_1_29_1","volume-title":"Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science 14, 4","author":"Orton Ian","year":"2018","unstructured":"Ian Orton and Andrew\u00a0 M. Pitts . 2018. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science 14, 4 ( 2018 ). https:\/\/doi.org\/10.23638\/LMCS-14(4:23)2018 arxiv:1712.04864 10.23638\/LMCS-14(4:23)2018 Ian Orton and Andrew\u00a0M. Pitts. 2018. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science 14, 4 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:23)2018 arxiv:1712.04864"},{"key":"e_1_3_2_1_30_1","unstructured":"The RedPRL Development Team. 2020. cooltt. http:\/\/www.github.com\/RedPRL\/cooltt  The RedPRL Development Team. 2020. cooltt. http:\/\/www.github.com\/RedPRL\/cooltt"},{"key":"e_1_3_2_1_31_1","volume-title":"Modalities in homotopy type theory. Logical Methods in Computer Science 16, 1","author":"Rijke Egbert","year":"2020","unstructured":"Egbert Rijke , Michael Shulman , and Bas Spitters . 2020. Modalities in homotopy type theory. Logical Methods in Computer Science 16, 1 ( 2020 ). arXiv:1706.07526 Egbert Rijke, Michael Shulman, and Bas Spitters. 2020. Modalities in homotopy type theory. Logical Methods in Computer Science 16, 1 (2020). arXiv:1706.07526"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_3_2_1_34_1","volume-title":"Workshop on the Implementation of Type Systems.","author":"Stassen Philipp","year":"2022","unstructured":"Philipp Stassen , Daniel Gratzer , and Lars Birkedal . 2022 . A flexible multimodal proof assistant . In Workshop on the Implementation of Type Systems. Philipp Stassen, Daniel Gratzer, and Lars Birkedal. 2022. A flexible multimodal proof assistant. In Workshop on the Implementation of Type Systems."},{"key":"#cr-split#-e_1_3_2_1_35_1.1","unstructured":"Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph.\u00a0D. Dissertation. https:\/\/doi.org\/10.5281\/zenodo.5709838 CMU technical report CMU-CS-21-142. 10.5281\/zenodo.5709838"},{"key":"#cr-split#-e_1_3_2_1_35_1.2","unstructured":"Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph.\u00a0D. Dissertation. https:\/\/doi.org\/10.5281\/zenodo.5709838 CMU technical report CMU-CS-21-142."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_1_37_1","volume-title":"Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. 68, 6","author":"Sterling Jonathan","year":"2021","unstructured":"Jonathan Sterling and Robert Harper . 2021. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. 68, 6 ( 2021 ). https:\/\/doi.org\/10.1145\/3474834 arXiv:2010.08599\u00a0[cs.PL] 10.1145\/3474834 Jonathan Sterling and Robert Harper. 2021. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. 68, 6 (2021). https:\/\/doi.org\/10.1145\/3474834 arXiv:2010.08599\u00a0[cs.PL]"},{"key":"e_1_3_2_1_38_1","volume-title":"Preliminary Proceedings of the APPSEM Workshop on Normalisation by Evaluation, O.\u00a0Danvy and P.\u00a0Dybjer (Eds.). Department of Computer Science","author":"Streicher Thomas","year":"1998","unstructured":"Thomas Streicher . 1998 . Categorical intuitions underlying semantic normalisation proofs . In Preliminary Proceedings of the APPSEM Workshop on Normalisation by Evaluation, O.\u00a0Danvy and P.\u00a0Dybjer (Eds.). Department of Computer Science , Aarhus University. Thomas Streicher. 1998. Categorical intuitions underlying semantic normalisation proofs. In Preliminary Proceedings of the APPSEM Workshop on Normalisation by Evaluation, O.\u00a0Danvy and P.\u00a0Dybjer (Eds.). Department of Computer Science, Aarhus University."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_40_1","volume-title":"A General Framework for the Semantics of Type Theory. (04","author":"Uemura Taichi","year":"2019","unstructured":"Taichi Uemura . 2019. A General Framework for the Semantics of Type Theory. (04 2019 ). arXiv:1904.04097\u00a0[math.CT] https:\/\/arxiv.org\/abs\/1904.04097 Taichi Uemura. 2019. A General Framework for the Semantics of Type Theory. (04 2019). arXiv:1904.04097\u00a0[math.CT] https:\/\/arxiv.org\/abs\/1904.04097"},{"key":"e_1_3_2_1_41_1","volume-title":"Types for Proofs and Programs","author":"Watkins Kevin","unstructured":"Kevin Watkins , Iliano Cervesato , Frank Pfenning , and David Walker . 2004. A Concurrent Logical Framework: The Propositional Fragment . In Types for Proofs and Programs , Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 355\u2013377. https:\/\/doi.org\/10.1007\/978-3-540-24849-1_23 10.1007\/978-3-540-24849-1_23 Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2004. A Concurrent Logical Framework: The Propositional Fragment. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 355\u2013377. https:\/\/doi.org\/10.1007\/978-3-540-24849-1_23"}],"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.3532398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3532398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:09Z","timestamp":1750186929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3532398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":41,"alternative-id":["10.1145\/3531130.3532398","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3532398","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"}}]}}