{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:18Z","timestamp":1750220658747,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":71,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394769","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"425-439","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure"],"prefix":"10.1145","author":[{"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[{"name":"Department of Computer Science and Technology, University of Cambridge, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philip","family":"Saville","sequence":"additional","affiliation":[{"name":"School of Informatics, University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1109\/LICS.2007.33"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1016\/j.entcs.2013.09.007"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1016\/0304-3975(94)00283-O"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01)","author":"Altenkirch T.","year":"1816","unstructured":"T. Altenkirch , P. Dybjer , M. Hofmannz , and P. Scott . 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts . In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01) . IEEE Computer Society, Washington, DC, USA, 303-. http:\/\/dl.acm.org\/citation.cfm?id=87 1816 .871869 T. Altenkirch, P. Dybjer, M. Hofmannz, and P. Scott. 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01). IEEE Computer Society, Washington, DC, USA, 303-. http:\/\/dl.acm.org\/citation.cfm?id=871816.871869"},{"key":"e_1_3_2_1_6_1","volume-title":"6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995","volume":"953","author":"Altenkirch T.","unstructured":"T. Altenkirch , M. Hofmann , and T. Streicher . 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science , 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995 , Proceedings , Vol. 953 . 182--199. T. Altenkirch, M. Hofmann, and T. Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, Vol. 953. 182--199."},{"key":"e_1_3_2_1_7_1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), D. Kesner and B. Pientka (Eds.)","volume":"52","author":"Altenkirch T.","year":"2016","unstructured":"T. Altenkirch and A. 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)), D. Kesner and B. 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 T. Altenkirch and A. 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)), D. Kesner and B. 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"},{"unstructured":"T. Altenkirch and A. Kaposi. 2017. Normalisation by Evaluation for Type Theory in Type Theory. Logical Methods in Computer Science Volume 13 Issue 4 (Oct. 2017). https:\/\/doi.org\/10.23638\/LMCS-13(4:1)2017    10.23638\/LMCS-13(4:1)2017\nT. Altenkirch and A. Kaposi. 2017. Normalisation by Evaluation for Type Theory in Type Theory. Logical Methods in Computer Science Volume 13 Issue 4 (Oct. 2017). https:\/\/doi.org\/10.23638\/LMCS-13(4:1)2017","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","volume-title":"Category Theory","author":"Awodey S.","unstructured":"S. Awodey . 2010. Category Theory ( 2 nd ed.). Number 52 in Oxford Logic Guides. Oxford University Press . S. Awodey. 2010. Category Theory (2nd ed.). Number 52 in Oxford Logic Guides. Oxford University Press.","edition":"2"},{"volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Balat V.","unstructured":"V. Balat , R. Di Cosmo , and M. Fiore . 2004. Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums . In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Venice, Italy) (POPL '04). Association for Computing Machinery, New York, NY, USA, 64--76. https:\/\/doi.org\/10.1145\/964001.964007 10.1145\/964001.964007 V. Balat, R. Di Cosmo, and M. Fiore. 2004. Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Venice, Italy) (POPL '04). Association for Computing Machinery, New York, NY, USA, 64--76. https:\/\/doi.org\/10.1145\/964001.964007","key":"e_1_3_2_1_10_1"},{"volume-title":"Reports of the Midwest Category Seminar","unstructured":"J.B\u00e9nabou. 1967. Introduction to bicategories . In Reports of the Midwest Category Seminar . Springer Berlin Heidelberg , Berlin, Heidelberg , 1--77. https:\/\/doi.org\/10.1007\/BFb0074299 10.1007\/BFb0074299 J.B\u00e9nabou. 1967. Introduction to bicategories. In Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, 1--77. https:\/\/doi.org\/10.1007\/BFb0074299","key":"e_1_3_2_1_11_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1109\/LICS.1991.151645"},{"volume-title":"Bicategories and distributors. Encyclopedia of Mathematics and its Applications","author":"Borceux F.","unstructured":"F. Borceux . 1994. Bicategories and distributors. Encyclopedia of Mathematics and its Applications , Vol. 1 . Cambridge University Press , 281--324. https:\/\/doi.org\/10.1017\/CBO9780511525858.009 10.1017\/CBO9780511525858.009 F. Borceux. 1994. Bicategories and distributors. Encyclopedia of Mathematics and its Applications, Vol. 1. Cambridge University Press, 281--324. https:\/\/doi.org\/10.1017\/CBO9780511525858.009","key":"e_1_3_2_1_13_1"},{"key":"e_1_3_2_1_14_1","first-page":"93","article-title":"Cartesian bicategories II","volume":"19","author":"Carboni A.","year":"2008","unstructured":"A. Carboni , G. M. Kelly , R. F. C. Walters , and R.J. Wood . 2008 . Cartesian bicategories II . Theory and Applications of Categories 19 , 6 (2008), 93 -- 124 . http:\/\/www.tac.mta.ca\/tac\/volumes\/19\/6\/19-06abs.html A. Carboni, G. M. Kelly, R. F. C. Walters, and R.J. Wood. 2008. Cartesian bicategories II. Theory and Applications of Categories 19, 6 (2008), 93--124. http:\/\/www.tac.mta.ca\/tac\/volumes\/19\/6\/19-06abs.html","journal-title":"Theory and Applications of Categories"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1016\/0022-4049(93)90035-R"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1016\/0022-4049(87)90121-6"},{"unstructured":"S. Castellan P. Clairambault S. Rideau and G. Winskel. 2017. Games and Strategies as Event Structures. Logical Methods in Computer Science 13 (2017).  S. Castellan P. Clairambault S. Rideau and G. Winskel. 2017. Games and Strategies as Event Structures. Logical Methods in Computer Science 13 (2017).","key":"e_1_3_2_1_17_1"},{"key":"e_1_3_2_1_18_1","first-page":"1","article-title":"Intuitionistic Model Constructions and Normalization Proofs","volume":"7","author":"Coquand T.","year":"1997","unstructured":"T. Coquand and P. Dybjer . 1997 . Intuitionistic Model Constructions and Normalization Proofs . Mathematical. Structures in Comp. Sci. 7 , 1 (Feb. 1997), 75--94. https:\/\/doi.org\/10.1017\/S0960129596002150 10.1017\/S0960129596002150 T. Coquand and P. Dybjer. 1997. Intuitionistic Model Constructions and Normalization Proofs. Mathematical. Structures in Comp. Sci. 7, 1 (Feb. 1997), 75--94. https:\/\/doi.org\/10.1017\/S0960129596002150","journal-title":"Mathematical. Structures in Comp. Sci."},{"volume-title":"Categories for Types","author":"Crole R. L.","unstructured":"R. L. Crole . 1994. Categories for Types . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9781139172707 10.1017\/CBO9781139172707 R. L. Crole. 1994. Categories for Types. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139172707","key":"e_1_3_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1017\/S0960129597002508"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1109\/LICS.2013.60"},{"volume-title":"Reports of the Midwest Category Seminar IV","author":"Day B.","unstructured":"B. Day . 1970. On closed categories of functors . In Reports of the Midwest Category Seminar IV , S. Mac Lane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 1--38. https:\/\/doi.org\/10.1007\/BFb0060438 10.1007\/BFb0060438 B. Day. 1970. On closed categories of functors. In Reports of the Midwest Category Seminar IV, S. Mac Lane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--38. https:\/\/doi.org\/10.1007\/BFb0060438","key":"e_1_3_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1006\/aima.1997.1649"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_25_1","volume-title":"Algebraic Foundations for Type Theories. 18th Types for Proofs and Programs workshop. Slides","author":"Fiore M.","year":"2011","unstructured":"M. Fiore . 2011 . Algebraic Foundations for Type Theories. 18th Types for Proofs and Programs workshop. Slides available at https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/Types2011.pdf. M. Fiore. 2011. Algebraic Foundations for Type Theories. 18th Types for Proofs and Programs workshop. Slides available at https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/Types2011.pdf."},{"volume-title":"Program on Higher Structures in Geometry and Physics","author":"Fiore M.","unstructured":"M. Fiore . 2016. An Algebraic Combinatorial Approach to Opetopic Structure. https:\/\/www.mpim-bonn.mpg.de\/node\/6586. Talk at the Seminar on Higher Structures , Program on Higher Structures in Geometry and Physics , Max Planck Institute for Mathematics , Bonn (Germany). M. Fiore. 2016. An Algebraic Combinatorial Approach to Opetopic Structure. https:\/\/www.mpim-bonn.mpg.de\/node\/6586. Talk at the Seminar on Higher Structures, Program on Higher Structures in Geometry and Physics, Max Planck Institute for Mathematics, Bonn (Germany).","key":"e_1_3_2_1_26_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1112\/jlms\/jdm096"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1007\/s00029-017-0361-3"},{"unstructured":"M. Fiore and A. Joyal. 2015. Theory of para-toposes. Talk at the Category Theory 2015 Conference. Departamento de Matematica Universidade de Aveiro (Portugal).  M. Fiore and A. Joyal. 2015. Theory of para-toposes. Talk at the Category Theory 2015 Conference. Departamento de Matematica Universidade de Aveiro (Portugal).","key":"e_1_3_2_1_29_1"},{"volume-title":"Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS '99)","author":"Fiore M.","unstructured":"M. Fiore , G. Plotkin , and D. Turi . 1999. Abstract Syntax and Variable Binding . In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS '99) . IEEE Computer Society, Washington, DC, USA, 193-. http:\/\/dl.acm.org\/citation.cfm?id=788021.788948 M. Fiore, G. Plotkin, and D. Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS '99). IEEE Computer Society, Washington, DC, USA, 193-. http:\/\/dl.acm.org\/citation.cfm?id=788021.788948","key":"e_1_3_2_1_30_1"},{"key":"e_1_3_2_1_31_1","volume-title":"List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017","author":"Fiore M.","year":"2017","unstructured":"M. Fiore and P. Saville . 2017 . List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 , September 3-9, 2017 , Oxford, UK. 16:1--16:18. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2017.16 10.4230\/LIPIcs.FSCD.2017.16 M. Fiore and P. Saville. 2017. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 16:1--16:18. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.16"},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '19)","author":"Fiore M.","year":"2019","unstructured":"M. Fiore and P. Saville . 2019. A type theory for cartesian closed bicategories . In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '19) . https:\/\/doi.org\/10.1109\/LICS. 2019 .8785708 10.1109\/LICS.2019.8785708 M. Fiore and P. Saville. 2019. A type theory for cartesian closed bicategories. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '19). https:\/\/doi.org\/10.1109\/LICS.2019.8785708"},{"doi-asserted-by":"crossref","unstructured":"M. Fiore and P. Saville. 2020. Relative Full Completeness for Bicategorical Cartesian Closed Structure. In Foundations of Software Science and Computation Structures J. Goubault-Larrecq and B. K\u00f6nig (Eds.). Springer International Publishing Cham. 277--298. https:\/\/doi.org\/10.1007\/978-3-030-45231-5_15 10.1007\/978-3-030-45231-5_15","key":"#cr-split#-e_1_3_2_1_33_1.1","DOI":"10.1007\/978-3-030-45231-5_15"},{"doi-asserted-by":"crossref","unstructured":"M. Fiore and P. Saville. 2020. Relative Full Completeness for Bicategorical Cartesian Closed Structure. In Foundations of Software Science and Computation Structures J. Goubault-Larrecq and B. K\u00f6nig (Eds.). Springer International Publishing Cham. 277--298. https:\/\/doi.org\/10.1007\/978-3-030-45231-5_15","key":"#cr-split#-e_1_3_2_1_33_1.2","DOI":"10.26226\/morressier.604907f51a80aac83ca25d68"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1090\/memo\/0860"},{"key":"e_1_3_2_1_35_1","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD '18) (Leibniz International Proceedings in Informatics (LIPIcs)), H. Kirchner (Ed.)","volume":"108","author":"Forest S.","year":"2018","unstructured":"S. Forest and S. Mimram . 2018. Coherence of Gray Categories via Rewriting . In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD '18) (Leibniz International Proceedings in Informatics (LIPIcs)), H. Kirchner (Ed.) , Vol. 108 . 15:1--15:16. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2018 .15 10.4230\/LIPIcs.FSCD.2018.15 S. Forest and S. Mimram. 2018. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD '18) (Leibniz International Proceedings in Informatics (LIPIcs)), H. Kirchner (Ed.), Vol. 108. 15:1--15:16. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.15"},{"key":"e_1_3_2_1_36_1","volume-title":"Memoirs of the AMS","volume":"249","author":"Gambino N.","unstructured":"N. Gambino and A. Joyal . 2017. On operads, bimodules and analytic functors . Memoirs of the AMS , Vol. 249 . American Mathematical Society. N. Gambino and A. Joyal. 2017. On operads, bimodules and analytic functors. Memoirs of the AMS, Vol. 249. American Mathematical Society."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1017\/S0305004112000394"},{"unstructured":"J.-Y. Girard P. Taylor and Y. Lafont. 1989. Proofs and Types. Cambridge University Press New York NY USA.  J.-Y. Girard P. Taylor and Y. Lafont. 1989. Proofs and Types. Cambridge University Press New York NY USA.","key":"e_1_3_2_1_39_1"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS '98)","author":"Cattani G.L.","year":"1998","unstructured":"G.L. Cattani , M. Fiore , and G. Winskel . 1998. A theory of recursive domains with applications to concurrency . In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS '98) . IEEE Computer Society, 214--225. https:\/\/doi.org\/10.1109\/LICS. 1998 .705658 10.1109\/LICS.1998.705658 G.L. Cattani, M. Fiore, and G. Winskel. 1998. A theory of recursive domains with applications to concurrency. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS '98). IEEE Computer Society, 214--225. https:\/\/doi.org\/10.1109\/LICS.1998.705658"},{"key":"e_1_3_2_1_41_1","volume-title":"Memoirs of the AMS","volume":"558","author":"Gordon R.","unstructured":"R. Gordon , A. J. Power , and R. Street . 1995. Coherence for tricategories . Memoirs of the AMS , Vol. 558 . American Mathematical Society. R. Gordon, A. J. Power, and R. Street. 1995. Coherence for tricategories. Memoirs of the AMS, Vol. 558. American Mathematical Society."},{"key":"e_1_3_2_1_42_1","series-title":"Lecture Notes in Mathematics","volume-title":"Formal Category Theory: Adjointness for 2-Categories","author":"Gray J. W.","unstructured":"J. W. Gray . 1974. Formal Category Theory: Adjointness for 2-Categories . Lecture Notes in Mathematics , Vol. 391 . Springer . https:\/\/doi.org\/10.1007\/BFb0061280 10.1007\/BFb0061280 J. W. Gray. 1974. Formal Category Theory: Adjointness for 2-Categories. Lecture Notes in Mathematics, Vol. 391. Springer. https:\/\/doi.org\/10.1007\/BFb0061280"},{"volume-title":"Coherence in Three-Dimensional Category Theory","author":"Gurski N.","unstructured":"N. Gurski . 2013. Coherence in Three-Dimensional Category Theory . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9781139542333 10.1017\/CBO9781139542333 N. Gurski. 2013. Coherence in Three-Dimensional Category Theory. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139542333","key":"e_1_3_2_1_43_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_44_1","DOI":"10.1016\/S0304-3975(96)00097-7"},{"key":"e_1_3_2_1_45_1","volume-title":"Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9 (Sept","author":"Hirschowitz T.","year":"2013","unstructured":"T. Hirschowitz . 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9 (Sept . 2013 ), 1--22. https:\/\/doi.org\/10.2168\/LMCS-9(3:10)2013 10.2168\/LMCS-9(3:10)2013 T. Hirschowitz. 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9 (Sept. 2013), 1--22. https:\/\/doi.org\/10.2168\/LMCS-9(3:10)2013"},{"doi-asserted-by":"crossref","unstructured":"A. Joyal and R. Street. 1993. Braided tensor categories. Advances in Mathematics 102 1 (11 1993) 20--78. https:\/\/doi.org\/10.1006\/aima.1993.1055 10.1006\/aima.1993.1055","key":"#cr-split#-e_1_3_2_1_47_1.1","DOI":"10.1006\/aima.1993.1055"},{"doi-asserted-by":"crossref","unstructured":"A. Joyal and R. Street. 1993. Braided tensor categories. Advances in Mathematics 102 1 (11 1993) 20--78. https:\/\/doi.org\/10.1006\/aima.1993.1055","key":"#cr-split#-e_1_3_2_1_47_1.2","DOI":"10.1006\/aima.1993.1055"},{"volume-title":"Springer New York","author":"Lack S.","unstructured":"S. Lack . 2010. A 2- Categories Companion . Springer New York , New York, NY , 105--191. https:\/\/doi.org\/10.1007\/978-1-4419-1524-5_4 10.1007\/978-1-4419-1524-5_4 S. Lack. 2010. A 2-Categories Companion. Springer New York, New York, NY, 105--191. https:\/\/doi.org\/10.1007\/978-1-4419-1524-5_4","key":"e_1_3_2_1_48_1"},{"key":"e_1_3_2_1_49_1","first-page":"1","article-title":"Bicategories of spans as cartesian bicategories","volume":"24","author":"Lack S.","year":"2010","unstructured":"S. Lack , R. F. C. Walters , and R. J. Wood . 2010 . Bicategories of spans as cartesian bicategories . Theory and Applications of Categories 24 , 1 (2010), 1 -- 24 . http:\/\/www.tac.mta.ca\/tac\/volumes\/24\/1\/24-01.pdf S. Lack, R. F. C. Walters, and R. J. Wood. 2010. Bicategories of spans as cartesian bicategories. Theory and Applications of Categories 24, 1 (2010), 1--24. http:\/\/www.tac.mta.ca\/tac\/volumes\/24\/1\/24-01.pdf","journal-title":"Theory and Applications of Categories"},{"unstructured":"J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Cambridge University Press New York NY USA.  J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Cambridge University Press New York NY USA.","key":"e_1_3_2_1_50_1"},{"key":"e_1_3_2_1_51_1","volume-title":"Basic Bicategories. (May","author":"Leinster T.","year":"1998","unstructured":"T. Leinster . 1998. Basic Bicategories. (May 1998 ). Available at https:\/\/arxiv.org\/abs\/math\/9810017. T. Leinster. 1998. Basic Bicategories. (May 1998). Available at https:\/\/arxiv.org\/abs\/math\/9810017."},{"key":"e_1_3_2_1_52_1","series-title":"Number 298 in London Mathematical Society Lecture Note Series","volume-title":"Higher operads, higher categories","author":"Leinster T.","unstructured":"T. Leinster . 2004. Higher operads, higher categories . Number 298 in London Mathematical Society Lecture Note Series . Cambridge University Press . T. Leinster. 2004. Higher operads, higher categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press."},{"doi-asserted-by":"crossref","unstructured":"Q. M. Ma and J. C. Reynolds. 1992. Types abstraction and parametric polymorphism part 2. In Mathematical Foundations of Programming Semantics S. Brookes M. Main A. Melton M. Mislove and D. Schmidt (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 1--40.  Q. M. Ma and J. C. Reynolds. 1992. Types abstraction and parametric polymorphism part 2. In Mathematical Foundations of Programming Semantics S. Brookes M. Main A. Melton M. Mislove and D. Schmidt (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 1--40.","key":"e_1_3_2_1_53_1","DOI":"10.1007\/3-540-55511-0_1"},{"key":"e_1_3_2_1_54_1","volume-title":"Natural associativity and commutativity","author":"Mac Lane S.","year":"1963","unstructured":"S. Mac Lane . 1963. Natural associativity and commutativity . Rice University Studies ( 1963 ). https:\/\/hdl.handle.net\/1911\/62865 S. Mac Lane. 1963. Natural associativity and commutativity. Rice University Studies (1963). https:\/\/hdl.handle.net\/1911\/62865"},{"volume-title":"Categories for the Working Mathematician","author":"Mac Lane S.","unstructured":"S. Mac Lane . 1998. Categories for the Working Mathematician ( second ed.). Graduate Texts in Mathematics, Vol. 5 . Springer-Verlag New York . https:\/\/doi.org\/10.1007\/978-1-4757-4721-8 10.1007\/978-1-4757-4721-8 S. Mac Lane. 1998. Categories for the Working Mathematician (second ed.). Graduate Texts in Mathematics, Vol. 5. Springer-Verlag New York. https:\/\/doi.org\/10.1007\/978-1-4757-4721-8","key":"e_1_3_2_1_55_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_56_1","DOI":"10.1016\/0022-4049(85)90087-8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_57_1","DOI":"10.1016\/0022-4049(95)00029-1"},{"volume-title":"Intersection Type Distributors. arXiv","year":"2020","unstructured":"Federico Olimpieri. 2020. Intersection Type Distributors. arXiv ( 2020 ). arXiv:2002.01287v2 [cs.LO] Federico Olimpieri. 2020. Intersection Type Distributors. arXiv (2020). arXiv:2002.01287v2 [cs.LO]","key":"e_1_3_2_1_58_1"},{"key":"e_1_3_2_1_59_1","volume-title":"A two-dimensional extension of Lambek's categorical proof theory. Master's thesis","author":"Ouaknine J.","year":"2027","unstructured":"J. Ouaknine . 1997. A two-dimensional extension of Lambek's categorical proof theory. Master's thesis . McGill University . http:\/\/digitool.library.mcgill.ca\/R\/?func=dbin-jump-full&object_id= 2027 7&local_base=GEN01-MCG02 J. Ouaknine. 1997. A two-dimensional extension of Lambek's categorical proof theory. Master's thesis. McGill University. http:\/\/digitool.library.mcgill.ca\/R\/?func=dbin-jump-full&object_id=20277&local_base=GEN01-MCG02"},{"key":"e_1_3_2_1_61_1","volume-title":"An elementary calculus of approximations (extended abstract). (1987). Unpublished manuscript","author":"Pitts A. M.","year":"1987","unstructured":"A. M. Pitts . 1987. An elementary calculus of approximations (extended abstract). (1987). Unpublished manuscript , University of Sussex , December 1987 . A. M. Pitts. 1987. An elementary calculus of approximations (extended abstract). (1987). Unpublished manuscript, University of Sussex, December 1987."},{"volume-title":"Handbook of Logic in Computer Science","author":"Pitts A. M.","unstructured":"A. M. Pitts . 2000. Categorical Logic . In Handbook of Logic in Computer Science . Oxford University Press , Oxford, UK , Chapter 2, 39--123. http:\/\/dl.acm.org\/citation.cfm?id=373919.373928 A. M. Pitts. 2000. Categorical Logic. In Handbook of Logic in Computer Science. Oxford University Press, Oxford, UK, Chapter 2, 39--123. http:\/\/dl.acm.org\/citation.cfm?id=373919.373928","key":"e_1_3_2_1_62_1"},{"key":"e_1_3_2_1_63_1","volume-title":"Coherence for Bicategories with Finite Bilimits I. In Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held","volume":"92","author":"Power A. J.","year":"1989","unstructured":"A. J. Power . 1989 . Coherence for Bicategories with Finite Bilimits I. In Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987 with Support from the National Science Foundation, J. W. Gray and A. Scedrov (Eds.). Vol. 92 . American Mathematical Society, 341--349. A. J. Power. 1989. Coherence for Bicategories with Finite Bilimits I. In Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987 with Support from the National Science Foundation, J. W. Gray and A. Scedrov (Eds.). Vol. 92. American Mathematical Society, 341--349."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_64_1","DOI":"10.1016\/0022-4049(89)90113-8"},{"volume-title":"On explicit substitutions and names (extended abstract)","author":"Ritter E.","unstructured":"E. Ritter and V. de Paiva . 1997. On explicit substitutions and names (extended abstract) . In Automata, Languages and Programming, P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 248--258. https:\/\/doi.org\/10.1007\/3-540-63165-8_182 10.1007\/3-540-63165-8_182 E. Ritter and V. de Paiva. 1997. On explicit substitutions and names (extended abstract). In Automata, Languages and Programming, P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 248--258. https:\/\/doi.org\/10.1007\/3-540-63165-8_182","key":"e_1_3_2_1_65_1"},{"key":"e_1_3_2_1_67_1","volume-title":"Proceedings of the 2nd Annual IEEE Symp. on Logic in Computer Science (LICS '87)","author":"Seely R. A. G.","year":"1987","unstructured":"R. A. G. Seely . 1987 . Modelling computations: a 2-categorical framework . In Proceedings of the 2nd Annual IEEE Symp. on Logic in Computer Science (LICS '87) (Ithaca, NY, USA), D. Gries (Ed.). IEEE Computer Society Press, 65--71. R. A. G. Seely. 1987. Modelling computations: a 2-categorical framework. In Proceedings of the 2nd Annual IEEE Symp. on Logic in Computer Science (LICS '87) (Ithaca, NY, USA), D. Gries (Ed.). IEEE Computer Society Press, 65--71."},{"key":"e_1_3_2_1_68_1","volume-title":"Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA","author":"Statman R.","year":"2014","unstructured":"R. Statman . 2014. Near semi-rings and lambda calculus . In Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014 , Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, G. Dowek (Ed.). Springer International Publishing , Cham., 410--424. https:\/\/doi.org\/10.1007\/978-3-319-08918-8_28 10.1007\/978-3-319-08918-8_28 R. Statman. 2014. Near semi-rings and lambda calculus. In Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, G. Dowek (Ed.). Springer International Publishing, Cham., 410--424. https:\/\/doi.org\/10.1007\/978-3-319-08918-8_28"},{"volume-title":"Foundations of Software Science and Computation Structures","author":"Staton S.","unstructured":"S. Staton . 2013. An algebraic presentation of predicate logic . In Foundations of Software Science and Computation Structures , F. Pfenning (Ed.). Springer Berlin Heidelberg, Berlin , Heidelberg , 401--417. https:\/\/doi.org\/10.1007\/978-3-642-37075-5_26 10.1007\/978-3-642-37075-5_26 S. Staton. 2013. An algebraic presentation of predicate logic. In Foundations of Software Science and Computation Structures, F. Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 401--417. https:\/\/doi.org\/10.1007\/978-3-642-37075-5_26","key":"e_1_3_2_1_69_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_70_1","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"e_1_3_2_1_71_1","first-page":"111","article-title":"Fibrations in bicategories","volume":"21","author":"Street R.","year":"1980","unstructured":"R. Street . 1980 . Fibrations in bicategories . Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 21 , 2 (1980), 111 -- 160 . http:\/\/eudml.org\/doc\/91227 R. Street. 1980. Fibrations in bicategories. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 21, 2 (1980), 111--160. http:\/\/eudml.org\/doc\/91227","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"volume-title":"Handbook of Algebra","author":"Street R.","unstructured":"R. Street . 1995. Categorical Structures . In Handbook of Algebra , M. Hazewinkel (Ed.). Vol. 1 . Elsevier , Chapter 15, 529--577. http:\/\/maths.mq.edu.au\/~street\/45.pdf R. Street. 1995. Categorical Structures. In Handbook of Algebra, M. Hazewinkel (Ed.). Vol. 1. Elsevier, Chapter 15, 529--577. http:\/\/maths.mq.edu.au\/~street\/45.pdf","key":"e_1_3_2_1_72_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_73_1","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_74_1","volume-title":"Coherence for Skew-Monoidal Categories. Electronic Proceedings in Theoretical Computer Science 153 (June","author":"Uustalu T.","year":"2014","unstructured":"T. Uustalu . 2014 . Coherence for Skew-Monoidal Categories. Electronic Proceedings in Theoretical Computer Science 153 (June 2014). https:\/\/doi.org\/10.4204\/EPTCS.153.5 10.4204\/EPTCS.153.5 T. Uustalu. 2014. Coherence for Skew-Monoidal Categories. Electronic Proceedings in Theoretical Computer Science 153 (June 2014). https:\/\/doi.org\/10.4204\/EPTCS.153.5"}],"event":{"sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"acronym":"LICS '20","name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany"},"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.3394769","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394769","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.3394769"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":71,"alternative-id":["10.1145\/3373718.3394769","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394769","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"}}]}}