{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:39Z","timestamp":1775790819619,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804,12386"],"award-info":[{"award-number":["25804,12386"]}],"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":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394736","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"492-506","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Multimodal Dependent Type Theory"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"name":"Aarhus University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G. A.","family":"Kavvos","sequence":"additional","affiliation":[{"name":"Aarhus University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Nuyts","sequence":"additional","affiliation":[{"name":"imec-DistriNet, KU Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006853"},{"key":"#cr-split#-e_1_3_2_1_3_1.1","doi-asserted-by":"crossref","unstructured":"Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8 1(2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:29)2012 10.2168\/LMCS-8(1:29)2012","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"#cr-split#-e_1_3_2_1_3_1.2","doi-asserted-by":"crossref","unstructured":"Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8 1(2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:29)2012","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_3_2_1_5_1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Delia Kesner and Brigitte Pientka (Eds.)","volume":"52","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)), Delia Kesner and Brigitte Pientka (Eds.) , Vol. 52 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1--6: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)), Delia Kesner and Brigitte Pientka (Eds.), Vol. 52. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1--6:16. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_3_2_1_7_1","volume-title":"27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Angiuli Carlo","year":"2018","unstructured":"Carlo Angiuli , Kuen-Bang Hou (Favonia), and Robert Harper . 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities . In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs)) , Dan Ghica and Achim Jung (Eds.), Vol. 119 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 6:1--6:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2018 .6 10.4230\/LIPIcs.CSL.2018.6 Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), Dan Ghica and Achim Jung (Eds.), Vol. 119. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1--6:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.6"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341713"},{"key":"e_1_3_2_1_12_1","volume-title":"On an Intuitionistic Modal Logic. Studia Logica 65, 3","author":"Bierman G. M.","year":"2000","unstructured":"G. M. Bierman and V. C. V. de Paiva . 2000. On an Intuitionistic Modal Logic. Studia Logica 65, 3 ( 2000 ). https:\/\/doi.org\/10.1023\/A: 1005291931660 10.1023\/A: G. M. Bierman and V. C. V. de Paiva. 2000. On an Intuitionistic Modal Logic. Studia Logica 65, 3 (2000). https:\/\/doi.org\/10.1023\/A: 1005291931660"},{"key":"e_1_3_2_1_13_1","volume-title":"Developing Theories of Types and Computability via Realizability. Electronic Notes in Theoretical Computer Science 34","author":"Birkedal Lars","year":"2000","unstructured":"Lars Birkedal . 2000. Developing Theories of Types and Computability via Realizability. Electronic Notes in Theoretical Computer Science 34 ( 2000 ). Lars Birkedal. 2000. Developing Theories of Types and Computability via Realizability. Electronic Notes in Theoretical Computer Science 34 (2000)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_1_15_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 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 ). https:\/\/doi.org\/10.2168\/LMCS-8(4:1)2012 10.2168\/LMCS-8(4:1)2012 Lars Birkedal, Rasmus 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). https:\/\/doi.org\/10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_1_16_1","volume-title":"Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal.","author":"Bizjak Ale\u0161","year":"2016","unstructured":"Ale\u0161 Bizjak , Hans Bugge Grathwohl , Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal. 2016 . Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg , 20--35. Ale\u0161 Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg, 20--35."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.007"},{"key":"e_1_3_2_1_19_1","volume-title":"Undecidability of Equality in the Free Locally Cartesian Closed Category. Logical Methods in Computer Science 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. Logical Methods in Computer Science 13, 4 ( 2017 ). https: \/\/doi.org\/10.23638\/LMCS-13(4:22)2017 10.23638\/LMCS-13(4:22)2017 Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2017. Undecidability of Equality in the Free Locally Cartesian Closed Category. Logical Methods in Computer Science 13, 4 (2017). https: \/\/doi.org\/10.23638\/LMCS-13(4:22)2017"},{"key":"e_1_3_2_1_20_1","volume-title":"Foundations of Software Science and Computation Structures","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 Lago (Eds.). Springer International Publishing , 258--275. Ranald Clouston. 2018. Fitch-Style Modal Lambda Calculi. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, 258--275."},{"key":"e_1_3_2_1_21_1","volume-title":"Hans Bugge Grathwohl, and Lars Birkedal","author":"Clouston Ranald","year":"2015","unstructured":"Ranald Clouston , Ale\u0161 Bizjak , Hans Bugge Grathwohl, and Lars Birkedal . 2015 . Programming and Reasoning with Guarded Recursion for Coinductive Types. In Foundations of Software Science and Computation Structures (Berlin, Heidelberg), Andrew Pitts (Ed.). Springer Berlin Heidelberg , 407--421. Ranald Clouston, Ale\u0161 Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2015. Programming and Reasoning with Guarded Recursion for Coinductive Types. In Foundations of Software Science and Computation Structures (Berlin, Heidelberg), Andrew Pitts (Ed.). Springer Berlin Heidelberg, 407--421."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)","author":"Coquand Thierry","year":"1986","unstructured":"Thierry Coquand . 1986 . An Analysis of Girard's Paradox . In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) (Cambridge, MA, USA). IEEE Computer Society Press, 227--236. Thierry Coquand. 1986. An Analysis of Girard's Paradox. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) (Cambridge, MA, USA). IEEE Computer Society Press, 227--236."},{"key":"e_1_3_2_1_23_1","unstructured":"Thierry Coquand. 2013. Presheaf model of type theory. http:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf  Thierry Coquand. 2013. Presheaf model of type theory. http:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf"},{"key":"e_1_3_2_1_24_1","unstructured":"Thierry Coquand. 2018. Canonicity and normalization for Dependent Type Theory. arXiv:1810.09367  Thierry Coquand. 2018. Canonicity and normalization for Dependent Type Theory. arXiv:1810.09367"},{"key":"e_1_3_2_1_25_1","first-page":"43","article-title":"Substitution up to isomorphism","volume":"23","author":"Curien P.-L.","year":"1990","unstructured":"P.-L. Curien . 1990 . Substitution up to isomorphism . Diagrammes 23 (1990), 43 -- 66 . http:\/\/www.numdam.org\/item\/DIA_1990_23_43_0 P.-L. Curien. 1990. Substitution up to isomorphism. Diagrammes 23 (1990), 43--66. http:\/\/www.numdam.org\/item\/DIA_1990_23_43_0","journal-title":"Diagrammes"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015","author":"de Paiva Valeria","year":"2015","unstructured":"Valeria de Paiva and Eike Ritter . 2015 . Fibrational Modal Type Theory , In Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015 ). Electronic Notes in Theoretical Computer Science. https:\/\/doi.org\/10.1016\/j.entcs. 2016.06.010 10.1016\/j.entcs.2016.06.010 Valeria de Paiva and Eike Ritter. 2015. Fibrational Modal Type Theory, In Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015). Electronic Notes in Theoretical Computer Science. https:\/\/doi.org\/10.1016\/j.entcs.2016.06.010"},{"key":"e_1_3_2_1_28_1","volume-title":"Types for Proofs and Programs","author":"Dybjer Peter","unstructured":"Peter Dybjer . 1996. Internal type theory . In Types for Proofs and Programs , Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 120--134. https:\/\/doi.org\/10.1007\/3-540-61780-9_66 10.1007\/3-540-61780-9_66 Peter Dybjer. 1996. Internal type theory. In Types for Proofs and Programs, Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 120--134. https:\/\/doi.org\/10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_1_29_1","volume-title":"Treatise on Intuitionistic Type Theory","author":"Granstr\u00f6m Johan Georg","unstructured":"Johan Georg Granstr\u00f6m and Johan Georg Granstr\u00f6m . 2011. Treatise on Intuitionistic Type Theory . Springer Netherlands . https:\/\/doi.org\/10.1007\/978-94-007-1736-7 10.1007\/978-94-007-1736-7 Johan Georg Granstr\u00f6m and Johan Georg Granstr\u00f6m. 2011. Treatise on Intuitionistic Type Theory. Springer Netherlands. https:\/\/doi.org\/10.1007\/978-94-007-1736-7"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_2_1_32_1","unstructured":"Jacob A Gross Daniel R Licata Max S New Jennifer Paykin Mitchell Riley Michael Shulman and Felix Wellen. 2017. Differential Cohesive Type Theory (Extended Abstract). In Extended abstracts for the Workshop \"Homotopy Type Theory and Univalent Foundations\". https:\/\/hott-uf.github.io\/2017\/abstracts\/cohesivett.pdf  Jacob A Gross Daniel R Licata Max S New Jennifer Paykin Mitchell Riley Michael Shulman and Felix Wellen. 2017. Differential Cohesive Type Theory (Extended Abstract). In Extended abstracts for the Workshop \"Homotopy Type Theory and Univalent Foundations\". https:\/\/hott-uf.github.io\/2017\/abstracts\/cohesivett.pdf"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_3_2_1_34_1","volume-title":"Semantics and Logics of Computation, Andrew M","author":"Hofmann Martin","unstructured":"Martin Hofmann . 1997. Syntax and Semantics of Dependent Types . In Semantics and Logics of Computation, Andrew M . Pitts and P. Dybjer (Eds.). Cambridge University Press , 79--130. 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 M. Pitts and P. Dybjer (Eds.). Cambridge University Press, 79--130. https:\/\/doi.org\/10.1017\/CBO9780511526619.004"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"},{"key":"e_1_3_2_1_36_1","unstructured":"B. Jacobs. 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland.  B. Jacobs. 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD","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 2019), Herman Geuvers (Ed.) , Vol. 131 . 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. 131."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290333"},{"key":"e_1_3_2_1_41_1","first-page":"41","article-title":"Axiomatic cohesion","volume":"19","author":"Lawvere F. William","year":"2007","unstructured":"F. William Lawvere . 2007 . Axiomatic cohesion . Theory and Applications of Categories 19 , 3 (2007), 41 -- 49 . http:\/\/www.tac.mta.ca\/tac\/volumes\/19\/3\/19-03 pdf F. William Lawvere. 2007. Axiomatic cohesion. Theory and Applications of Categories 19, 3 (2007), 41--49. http:\/\/www.tac.mta.ca\/tac\/volumes\/19\/3\/19-03 pdf","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_1_42_1","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Licata Daniel R.","year":"2018","unstructured":"Daniel R. Licata , Ian Orton , Andrew M. Pitts , and Bas 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)) , H. Kirchner (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik , 22:1--22:17. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2018 .22 arXiv:1801.07664 10.4230\/LIPIcs.FSCD.2018.22 Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas 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)), H. Kirchner (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 22:1--22:17. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.22 arXiv:1801.07664"},{"key":"e_1_3_2_1_43_1","volume-title":"Licata and Michael Shulman","author":"Daniel","year":"2016","unstructured":"Daniel R. Licata and Michael Shulman . 2016 . Adjoint Logic with a 2-Category of Modes. In Logical Foundations of Computer Science, Sergei Artemov and Anil Nerode (Eds.). Springer International Publishing , 219--235. https:\/\/doi.org\/10.1007\/978-3-319-27683-0_16 10.1007\/978-3-319-27683-0_16 Daniel R. Licata and Michael Shulman. 2016. Adjoint Logic with a 2-Category of Modes. In Logical Foundations of Computer Science, Sergei Artemov and Anil Nerode (Eds.). Springer International Publishing, 219--235. https:\/\/doi.org\/10.1007\/978-3-319-27683-0_16"},{"key":"e_1_3_2_1_44_1","volume-title":"2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Dale Miller (Ed.)","volume":"84","author":"Licata Daniel R.","year":"2017","unstructured":"Daniel 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)), Dale Miller (Ed.) , Vol. 84 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 25:1--25:22. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2017.25 10.4230\/LIPIcs.FSCD.2017.25 Daniel 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)), Dale Miller (Ed.), Vol. 84. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 25:1--25:22. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.25"},{"key":"e_1_3_2_1_45_1","unstructured":"Zhaohui Luo. 2012. Notes on Universes in Type Theory. http:\/\/www.dcs.rhul.ac.uk\/home\/zhaohui\/universes.pdf Notes for a talk at Institute for Advanced Study in Princeton in Oct 2012.  Zhaohui Luo. 2012. Notes on Universes in Type Theory. http:\/\/www.dcs.rhul.ac.uk\/home\/zhaohui\/universes.pdf Notes for a talk at Institute for Advanced Study in Princeton in Oct 2012."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_1_47_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_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_49_1","volume-title":"Mitchell and Andre Scedrov","author":"John","year":"1993","unstructured":"John C. Mitchell and Andre Scedrov . 1993 . Notes on sconing and relators. In Computer Science Logic, E. B\u00f6rger, G. J\u00e4ger, H. Kleine B\u00fcning, S. Martini, and M. M. Richter (Eds.). Springer Berlin Heidelberg , 352--378. https:\/\/doi.org\/10.1007\/3-540-56992-8_21 10.1007\/3-540-56992-8_21 John C. Mitchell and Andre Scedrov. 1993. Notes on sconing and relators. In Computer Science Logic, E. B\u00f6rger, G. J\u00e4ger, H. Kleine B\u00fcning, S. Martini, and M. M. Richter (Eds.). Springer Berlin Heidelberg, 352--378. https:\/\/doi.org\/10.1007\/3-540-56992-8_21"},{"key":"#cr-split#-e_1_3_2_1_50_1.1","doi-asserted-by":"crossref","unstructured":"Rasmus Ejlers M\u00f8gelberg. 2014. A Type Theory for Productive Coprogramming via Guarded Recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS '14). https: \/\/doi.org\/10.1145\/2603088.2603132 10.1145\/2603088.2603132","DOI":"10.1145\/2603088.2603132"},{"key":"#cr-split#-e_1_3_2_1_50_1.2","doi-asserted-by":"crossref","unstructured":"Rasmus Ejlers M\u00f8gelberg. 2014. A Type Theory for Productive Coprogramming via Guarded Recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS '14). https: \/\/doi.org\/10.1145\/2603088.2603132","DOI":"10.1145\/2603088.2603132"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_53_1","unstructured":"Andreas Nuyts. 2018. Presheaf Models of Relational Modalities in Dependent Type Theory. arXiv:1805.08684  Andreas Nuyts. 2018. Presheaf Models of Relational Modalities in Dependent Type Theory. arXiv:1805.08684"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_2_1_56_1","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Palmgren Erik","unstructured":"Erik Palmgren . 1998. On universes in type theory . In Twenty Five Years of Constructive Type Theory , G. Sambin and J. Smith (Eds.). Oxford University Press , 191--204. http:\/\/www2.math.uu.se\/~palmgren\/universe. pdf Erik Palmgren. 1998. On universes in type theory. In Twenty Five Years of Constructive Type Theory, G. Sambin and J. Smith (Eds.). Oxford University Press, 191--204. http:\/\/www2.math.uu.se\/~palmgren\/universe. pdf"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785683"},{"key":"e_1_3_2_1_60_1","unstructured":"Dag Prawitz. 1965. Natural Deduction: a proof-theoretical study. Almquist and Wiksell.  Dag Prawitz. 1965. Natural Deduction: a proof-theoretical study. Almquist and Wiksell."},{"key":"e_1_3_2_1_61_1","unstructured":"Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. (2009). http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf  Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. (2009). http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf"},{"key":"e_1_3_2_1_62_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_63_1","first-page":"81","article-title":"The free adjunction","volume":"27","author":"Schanuel Stephen","year":"1986","unstructured":"Stephen Schanuel and Ross Street . 1986 . The free adjunction . Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 27 , 1 (1986), 81 -- 83 . http:\/\/www.numdam.org\/item\/CTGDC_1986_27_1_81_0 Stephen Schanuel and Ross Street. 1986. The free adjunction. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 27, 1 (1986), 81--83. http:\/\/www.numdam.org\/item\/CTGDC_1986_27_1_81_0","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_3_2_1_64_1","unstructured":"Urs Schreiber. 2013. Differential cohomology in a cohesive infinity-topos. (2013). arXiv:1310.7930  Urs Schreiber. 2013. Differential cohomology in a cohesive infinity-topos. (2013). arXiv:1310.7930"},{"key":"e_1_3_2_1_65_1","volume-title":"Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012","author":"Schreiber Urs","year":"2012","unstructured":"Urs Schreiber and Michael Shulman . 2012 . Quantum Gauge Field Theory in Cohesive Homotopy Type Theory . In Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012 , Brussels, Belgium , 10-12 October 2012 (EPTCS), Ross Duncan and Prakash Panangaden (Eds.), Vol. 158. 109--126. https:\/\/doi.org\/10.4204\/EPTCS.158.8 10.4204\/EPTCS.158.8 Urs Schreiber and Michael Shulman. 2012. Quantum Gauge Field Theory in Cohesive Homotopy Type Theory. In Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012, Brussels, Belgium, 10-12 October 2012 (EPTCS), Ross Duncan and Prakash Panangaden (Eds.), Vol. 158. 109--126. https:\/\/doi.org\/10.4204\/EPTCS.158.8"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_3_2_1_68_1","unstructured":"Jonathan Sterling. 2019. Algebraic Type Theory and Universe Hierarchies. (2019). arXiv:1902.08848  Jonathan Sterling. 2019. Algebraic Type Theory and Universe Hierarchies. (2019). arXiv:1902.08848"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_70_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 . https:\/\/homotopytypetheory.org\/book The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_2_1_71_1","volume-title":"Natural Model Semantics for Comonadic and Adjoint Type Theory: Extended Abstract. In Preproceedings of Applied Category Theory Conference","author":"Zwanziger Colin","year":"2019","unstructured":"Colin Zwanziger . 2019 . Natural Model Semantics for Comonadic and Adjoint Type Theory: Extended Abstract. In Preproceedings of Applied Category Theory Conference 2019. Colin Zwanziger. 2019. Natural Model Semantics for Comonadic and Adjoint Type Theory: Extended Abstract. In Preproceedings of Applied Category Theory Conference 2019."}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394736","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394736","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394736"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":68,"alternative-id":["10.1145\/3373718.3394736","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394736","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}