{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:08Z","timestamp":1750183808447,"version":"3.41.0"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T00:00:00Z","timestamp":1674864000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Giuseppe Greco and Alessandra Palmigiano"},{"name":"NWO","award":["KIVI.2019.001"],"award-info":[{"award-number":["KIVI.2019.001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,4,30]]},"abstract":"<jats:p>\n            We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity.\n            <jats:italic>Properness<\/jats:italic>\n            (i.e.,\u00a0closure under uniform substitution of all parametric parts in rules) is the main technical novelty of the present proposal, allowing both for the smoothest proof of cut elimination and for the development of an overarching and modular treatment for a vast class of axiomatic extensions and expansions of intuitionistic, bi-intuitionistic, and classical linear logics with exponentials. Our proposal builds on an algebraic and order-theoretic analysis of linear logic and applies the guidelines of the multi-type methodology in the design of display calculi.\n          <\/jats:p>","DOI":"10.1145\/3570919","type":"journal-article","created":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T11:57:20Z","timestamp":1667822240000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Linear Logic Properly Displayed"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4845-3821","authenticated-orcid":false,"given":"Giuseppe","family":"Greco","sequence":"first","affiliation":[{"name":"School of Business and Economics, Vrije Universiteit Amsterdam, Amsterdam, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9656-7527","authenticated-orcid":false,"given":"Alessandra","family":"Palmigiano","sequence":"additional","affiliation":[{"name":"School of Business and Economics, Vrije Universiteit Amsterdam, The Netherlands and Department of Mathematics and Applied Mathematics, University of Johannesburg, Johannesburg, South Africa"}]}],"member":"320","published-online":{"date-parts":[[2023,1,28]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli Jean-Marc","year":"1992","unstructured":"Jean-Marc Andreoli. 1992. Logic programming with focusing proofs in linear logic. J. Logic Computat. 2 (1992), 297\u2013347.","journal-title":"J. Logic Computat."},{"issue":"1","key":"e_1_3_3_3_2","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/504077.504081","article-title":"Intuitionistic light affine logic","volume":"3","author":"Asperti Andrea","year":"2002","unstructured":"Andrea Asperti and Luca Roversi. 2002. Intuitionistic light affine logic. ACM Trans. Computat. Logic 3, 1 (2002), 137\u2013175.","journal-title":"ACM Trans. Computat. Logic"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(88)90037-0","article-title":"The semantics and proof theory of linear logic","volume":"57","author":"Avron Arnon","year":"1998","unstructured":"Arnon Avron. 1998. The semantics and proof theory of linear logic. Theoret. Comput. Sci. 57 (1998), 161\u2013184.","journal-title":"Theoret. Comput. Sci."},{"issue":"6","key":"e_1_3_3_5_2","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1093\/logcom\/13.6.835","article-title":"Hypersequent calculi for G\u00f6del logics\u2014A survey","volume":"13","author":"Baaz Matthias","year":"2003","unstructured":"Matthias Baaz, Agata Ciabattoni, and Christian G. Ferm\u00fcller. 2003. Hypersequent calculi for G\u00f6del logics\u2014A survey. J. Logic Computat. 13, 6 (2003), 835\u2013861.","journal-title":"J. Logic Computat."},{"key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.ic.2014.10.005","article-title":"On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy","volume":"241","author":"Baillot Patrick","year":"2015","unstructured":"Patrick Baillot. 2015. On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy. Inf. Comput. 241 (2015), 3\u201331.","journal-title":"Inf. Comput."},{"key":"e_1_3_3_7_2","unstructured":"Samuel Balco Giuseppe Greco Alexander Kurz M. Andrew Moshier Alessandra Palmigiano and Apostolos Tzimoulis. 2022. First Order Logic Properly Displayed. Submitted. arXiv:2105.06877."},{"issue":"4","key":"e_1_3_3_8_2","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","article-title":"Display logic","volume":"11","author":"Belnap Nuel D.","year":"1982","unstructured":"Nuel D. Belnap. 1982. Display logic. J. Philos. Logic 11, 4 (1982), 375\u2013417.","journal-title":"J. Philos. Logic"},{"issue":"1","key":"e_1_3_3_9_2","first-page":"14","article-title":"Linear logic displayed","volume":"31","author":"Belnap Nuel D.","year":"1990","unstructured":"Nuel D. Belnap. 1990. Linear logic displayed. Notre Dame J. Form. Logic 31, 1 (1990), 14\u201325.","journal-title":"Notre Dame J. Form. Logic"},{"key":"e_1_3_3_10_2","first-page":"121","volume-title":"International Workshop on Computer Science Logic","author":"Benton Nick","year":"1994","unstructured":"Nick Benton. 1994. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic. Springer, 121\u2013135."},{"key":"e_1_3_3_11_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"International Conference on Typed Lambda Calculi and Applications","author":"Benton Nick","year":"1993","unstructured":"Nick Benton, Gavin Bierman, Valeria De Paiva, and Martin Hyland. 1993. A term calculus for intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications. Springer, 75\u201390."},{"issue":"2","key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1017\/S175502031700034X","article-title":"The logic of resources and capabilities","volume":"11","author":"B\u00edlkov\u00e1 Marta","year":"2018","unstructured":"Marta B\u00edlkov\u00e1, Giuseppe Greco, Alessandra Palmigiano, Apostolos Tzimoulis, and Nachoem M. Wijnberg. 2018. The logic of resources and capabilities. Rev. Symb. Logic 11, 2 (2018), 371\u2013410.","journal-title":"Rev. Symb. Logic"},{"issue":"1","key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0021-9800(70)80014-X","article-title":"Heterogeneous algebras","volume":"8","author":"Birkhoff Garrett","year":"1970","unstructured":"Garrett Birkhoff and John D. Lipson. 1970. Heterogeneous algebras. J. Combinat. Theor. 8, 1 (1970), 115\u2013133.","journal-title":"J. Combinat. Theor."},{"key":"e_1_3_3_14_2","volume-title":"Modal Logic: Graph. Darst","author":"Blackburn Patrick","year":"2002","unstructured":"Patrick Blackburn, Maarten De Rijke, and Yde Venema. 2002. Modal Logic: Graph. Darst. Vol. 53. Cambridge University Press."},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","first-page":"104756","DOI":"10.1016\/j.ic.2021.104756","article-title":"Non-normal modal logics and conditional logics: Semantic analysis and proof theory","volume":"287","author":"Chen Jinsheng","year":"2021","unstructured":"Jinsheng Chen, Giuseppe Greco, Alessandra Palmigiano, and Apostolos Tzimoulis. 2021. Non-normal modal logics and conditional logics: Semantic analysis and proof theory. Inf. Computat. 287 (2021), 104756.","journal-title":"Inf. Computat."},{"issue":"4","key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3529255","article-title":"Syntactic completeness of proper display calculi","volume":"23","author":"Chen Jinsheng","year":"2022","unstructured":"Jinsheng Chen, Giuseppe Greco, Alessandra Palmigiano, and Apostolos Tzimoulis. 2022. Syntactic completeness of proper display calculi. ACM Trans. Computat. Logic 23, 4 (Mar.2022), 1\u201346.","journal-title":"ACM Trans. Computat. Logic"},{"key":"e_1_3_3_17_2","first-page":"229","volume-title":"23rd Annual IEEE Symposium on Logic in Computer Science","author":"Ciabattoni Agata","year":"2008","unstructured":"Agata Ciabattoni, Nikolas Galatos, and Terui Kazushige. 2008. From axioms to analytic rules in nonclassical logics, In 23rd Annual IEEE Symposium on Logic in Computer Science. 229\u2013240."},{"key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-642-39992-3_10","volume-title":"20th International Workshop on Logic, Language, Information, and Computation (Lecture Notes in Computer Science)","author":"Ciabattoni Agata","year":"2013","unstructured":"Agata Ciabattoni and Revantha Ramanayake. 2013. Structural extensions of display calculi: A general recipe. In 20th International Workshop on Logic, Language, Information, and Computation (Lecture Notes in Computer Science). Springer, 81\u201395."},{"issue":"3","key":"e_1_3_3_19_2","first-page":"17","article-title":"Power and limits of structural display rules","volume":"17","author":"Ciabattoni Agata","year":"2016","unstructured":"Agata Ciabattoni and Revantha Ramanayake. 2016. Power and limits of structural display rules. ACM Trans. Computat. Logic 17, 3 (2016), 17.","journal-title":"ACM Trans. Computat. Logic"},{"key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-662-55386-2_7","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Conradie Willem","year":"2017","unstructured":"Willem Conradie, Andrew Craig, Alessandra Palmigiano, and Zhiguang Zhao. 2017. Constructive canonicity for lattice-based fixed point logics. In International Workshop on Logic, Language, Information, and Computation. Springer, 92\u2013109."},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.tcs.2014.10.027","article-title":"Algorithmic correspondence for intuitionistic modal mu-calculus","volume":"564","author":"Conradie Willem","year":"2015","unstructured":"Willem Conradie, Yves Fomatati, Alessandra Palmigiano, and Sumit Sourabh. 2015. Algorithmic correspondence for intuitionistic modal mu-calculus. Theoret. Comput. Sci. 564 (2015), 30\u201362.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-662-52921-8_10","volume-title":"23rd International Workshop on Logic, Language, Information, and Computation","author":"Conradie Willem","year":"2016","unstructured":"Willem Conradie, Sabine Frittella, Alessandra Palmigiano, Michele Piazzai, Apostolos Tzimoulis, and Nachoem M. Wijnberg. 2016. Categories: How I learned to stop worrying and love two sorts. In 23rd International Workshop on Logic, Language, Information, and Computation. Springer, 145\u2013164. ArXiv preprint 1604.00777."},{"key":"e_1_3_3_23_2","series-title":"(Outstanding Contributions to Logic","doi-asserted-by":"crossref","first-page":"933","DOI":"10.1007\/978-3-319-06025-5_36","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"Conradie Willem","year":"2014","unstructured":"Willem Conradie, Silvio Ghilardi, and Alessandra Palmigiano. 2014. Unified correspondence. In Johan van Benthem on Logic and Information Dynamics(Outstanding Contributions to Logic, Vol. 5). Springer International Publishing, 933\u2013975."},{"issue":"3","key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/j.apal.2011.10.004","article-title":"Algorithmic correspondence and canonicity for distributive modal logic","volume":"163","author":"Conradie Willem","year":"2012","unstructured":"Willem Conradie and Alessandra Palmigiano. 2012. Algorithmic correspondence and canonicity for distributive modal logic. Ann. Pure Appl. Logic 163, 3 (2012), 338\u2013376.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"9","key":"e_1_3_3_25_2","doi-asserted-by":"crossref","first-page":"923","DOI":"10.1016\/j.apal.2019.04.003","article-title":"Algorithmic correspondence and canonicity for non-distributive logics","volume":"170","author":"Conradie Willem","year":"2019","unstructured":"Willem Conradie and Alessandra Palmigiano. 2019. Algorithmic correspondence and canonicity for non-distributive logics. Ann. Pure Appl. Logic 170, 9 (2019), 923\u2013974.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"e_1_3_3_26_2","first-page":"1","article-title":"Constructive canonicity of inductive inequalities","volume":"16","author":"Conradie Willem","year":"2020","unstructured":"Willem Conradie and Alessandra Palmigiano. 2020. Constructive canonicity of inductive inequalities. Logic. Meth. Comput. Sci. 16, 3 (2020), 1\u201339. arXiv:1603.08341.","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.jlamp.2016.10.006","article-title":"Algebraic modal correspondence: Sahlqvist and beyond","volume":"91","author":"Conradie Willem","year":"2017","unstructured":"Willem Conradie, Alessandra Palmigiano, and Sumit Sourabh. 2017. Algebraic modal correspondence: Sahlqvist and beyond. J. Logic. Algeb. Meth. Program. 91 (2017), 60\u201384.","journal-title":"J. Logic. Algeb. Meth. Program."},{"issue":"1","key":"e_1_3_3_28_2","first-page":"1","article-title":"Sahlqvist via translation","volume":"15","author":"Conradie Willem","year":"2019","unstructured":"Willem Conradie, Alessandra Palmigiano, and Zhiguang Zhao. 2019. Sahlqvist via translation. Logic. Meth. Comput. Sci. 15, 1 (2019), 1\u201335. ArXiv preprint 1603.08220.","journal-title":"Logic. Meth. Comput. Sci."},{"issue":"3","key":"e_1_3_3_29_2","first-page":"867","article-title":"On Sahlqvist theory for hybrid logic","volume":"27","author":"Conradie Willem","year":"2017","unstructured":"Willem Conradie and Claudette Robinson. 2017. On Sahlqvist theory for hybrid logic. J. Logic Computat. 27, 3 (2017), 867\u2013900.","journal-title":"J. Logic Computat."},{"issue":"5","key":"e_1_3_3_30_2","first-page":"1","article-title":"Light logics and the call-by-value lambda calculus","volume":"4","author":"Coppola Paolo","year":"2008","unstructured":"Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca. 2008. Light logics and the call-by-value lambda calculus. Logic. Meth. Comput. Sci. 4, 5 (2008), 1\u201328.","journal-title":"Logic. Meth. Comput. Sci."},{"issue":"1","key":"e_1_3_3_31_2","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.jal.2013.07.005","article-title":"Relational semantics for full linear logic","volume":"12","author":"Coumans Dion","year":"2014","unstructured":"Dion Coumans, Mai Gehrke, and Lorijn van Rooijen. 2014. Relational semantics for full linear logic. J. Appl. Logic 12, 1 (2014), 50\u201366.","journal-title":"J. Appl. Logic"},{"key":"e_1_3_3_32_2","volume-title":"Lattices and Order","author":"Davey Brian A.","year":"2002","unstructured":"Brian A. Davey and Hilary A. Priestley. 2002. Lattices and Order. Cambridge University Press."},{"issue":"3","key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3460973","article-title":"Slanted canonicity of analytic inductive inequalities","volume":"22","author":"Rudder Laurent De","year":"2021","unstructured":"Laurent De Rudder and Alessandra Palmigiano. 2021. Slanted canonicity of analytic inductive inequalities. ACM Trans. Computat. Logic 22, 3 (2021), 1\u201341.","journal-title":"ACM Trans. Computat. Logic"},{"issue":"3","key":"e_1_3_3_34_2","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF00260931","article-title":"Modal translations in substructural logics","volume":"21","author":"Do\u0161en Kosta","year":"1992","unstructured":"Kosta Do\u0161en. 1992. Modal translations in substructural logics. J. Philos. Logic 21, 3 (1992), 283\u2013336.","journal-title":"J. Philos. Logic"},{"issue":"2","key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.2307\/2964753","article-title":"A propositional calculus with denumerable matrix","volume":"24","author":"Dummett Michael","year":"1959","unstructured":"Michael Dummett. 1959. A propositional calculus with denumerable matrix. J. Symb. Logic 24, 2 (1959), 97\u2013106.","journal-title":"J. Symb. Logic"},{"issue":"2","key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/BF01061239","article-title":"Positive modal logic","volume":"55","author":"Dunn J. Michael","year":"1995","unstructured":"J. Michael Dunn. 1995. Positive modal logic. Studia Logica 55, 2 (1995), 301\u2013317.","journal-title":"Studia Logica"},{"issue":"3","key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"713","DOI":"10.2178\/jsl\/1122038911","article-title":"Canonical extensions and relational completeness of some structural logics","volume":"70","author":"Dunn J. Michael","year":"2005","unstructured":"J. Michael Dunn, Mai Gehrke, and Alessandra Palmigiano. 2005. Canonical extensions and relational completeness of some structural logics. J. Symb. Logic 70, 3 (2005), 713\u2013740.","journal-title":"J. Symb. Logic"},{"issue":"1","key":"e_1_3_3_38_2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1002\/malq.19710170126","article-title":"Algebraic completeness results for Dummetts LC and its extensions","volume":"17","author":"Dunn J. Michael","year":"1971","unstructured":"J. Michael Dunn and Robert K. Meyer. 1971. Algebraic completeness results for Dummetts LC and its extensions. Math. Logic Quart. 17, 1 (1971), 225\u2013230.","journal-title":"Math. Logic Quart."},{"key":"e_1_3_3_39_2","first-page":"995","volume-title":"Formal Models and Semantics","author":"Emerson E. Allen","year":"1990","unstructured":"E. Allen Emerson. 1990. Temporal and modal logic. In Formal Models and Semantics. Elsevier, 995\u20131072."},{"issue":"425","key":"e_1_3_3_40_2","first-page":"219","article-title":"Kurt G\u00f6del: Collected works, Vol. I: Publications 1929\u20131936","volume":"107","author":"Feferman Solomon","year":"1998","unstructured":"Solomon Feferman, John W. Dawson, Stephen C. Kleene, Gregory H. Moore, and Robert M. Solovay. 1998. Kurt G\u00f6del: Collected works, Vol. I: Publications 1929\u20131936. Mind 107, 425 (1998), 219\u2013232.","journal-title":"Mind"},{"issue":"6","key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"2067","DOI":"10.1093\/logcom\/exu064","article-title":"Multi-type display calculus for propositional dynamic logic","volume":"26","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alexander Kurz, and Alessandra Palmigiano. 2016. Multi-type display calculus for propositional dynamic logic. J. Logic Computat. 26, 6 (2016), 2067\u20132104.","journal-title":"J. Logic Computat."},{"issue":"6","key":"e_1_3_3_42_2","doi-asserted-by":"crossref","first-page":"2067","DOI":"10.1093\/logcom\/exu064","article-title":"Multi-type display calculus for propositional dynamic logic","volume":"26","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alexander Kurz, and Alessandra Palmigiano. 2016. Multi-type display calculus for propositional dynamic logic. J. Logic Computat. 26, 6 (2016), 2067\u20132104.","journal-title":"J. Logic Computat."},{"key":"e_1_3_3_43_2","first-page":"81","volume-title":"Proceedings Trends in Logic XIII","volume":"13","author":"Frittella Sabine","year":"2014","unstructured":"Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, and Vlasta Sikimi\u0107. 2014. Multi-type sequent calculi. In Proceedings Trends in Logic XIII, Vol. 13. \u0141\u00f3d\u017a University Press, 81\u201393."},{"issue":"6","key":"e_1_3_3_44_2","doi-asserted-by":"crossref","first-page":"2017","DOI":"10.1093\/logcom\/exu068","article-title":"Multi-type display calculus for dynamic epistemic logic","volume":"26","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, and Vlasta Sikimi\u0107. 2016. Multi-type display calculus for dynamic epistemic logic. J. Logic Computat. 26, 6 (2016), 2017\u20132065.","journal-title":"J. Logic Computat."},{"issue":"6","key":"e_1_3_3_45_2","doi-asserted-by":"crossref","first-page":"1961","DOI":"10.1093\/logcom\/exu063","article-title":"A proof-theoretic semantic analysis of dynamic epistemic logic","volume":"26","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, and Vlasta Sikimi\u0107. 2016. A proof-theoretic semantic analysis of dynamic epistemic logic. J. Logic Computat. 26, 6 (2016), 1961\u20132015.","journal-title":"J. Logic Computat."},{"key":"e_1_3_3_46_2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-662-52921-8_14","volume-title":"23rd International Workshop on Logic, Language, Information, and Computation (LNCS, Vol. 9803)","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alessandra Palmigiano, and Fan Yang. 2016. A multi-type calculus for inquisitive logic. In 23rd International Workshop on Logic, Language, Information, and Computation (LNCS, Vol. 9803). Springer, 215\u2013233."},{"issue":"1","key":"e_1_3_3_47_2","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1006\/jabr.2000.8622","article-title":"Bounded lattice expansions","volume":"238","author":"Gehrke Mai","year":"2001","unstructured":"Mai Gehrke and John Harding. 2001. Bounded lattice expansions. J. Algeb. 238, 1 (2001), 345\u2013371.","journal-title":"J. Algeb."},{"key":"e_1_3_3_48_2","first-page":"63","volume-title":"Conference on Mathematical Logic","author":"Ghilardi Silvio","year":"1988","unstructured":"Silvio Ghilardi and Gian Carlo Meloni. 1988. A category-theoretical approach to modal predicate and distributive linear logic (Italian). In Conference on Mathematical Logic. 63\u201368."},{"issue":"3","key":"e_1_3_3_49_2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1002\/malq.19900360303","article-title":"Modal logics with n-ary connectives","volume":"36","author":"Ghilardi Silvio","year":"1990","unstructured":"Silvio Ghilardi and Gian Carlo Meloni. 1990. Modal logics with n-ary connectives. Math. Logic Quart. 36, 3 (1990), 193\u2013215.","journal-title":"Math. Logic Quart."},{"issue":"1","key":"e_1_3_3_50_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard Jean-Yves","year":"1987","unstructured":"Jean-Yves Girard. 1987. Linear logic. Theoret. Comput. Sci. 50, 1 (1987), 1\u2013101.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_3_51_2","volume-title":"Proof Theory and Logical Complexity","author":"Girard Jean-Yves","year":"1987","unstructured":"Jean-Yves Girard. 1987. Proof Theory and Logical Complexity, Vol. 1. Humanities Press."},{"issue":"3","key":"e_1_3_3_52_2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","article-title":"On the unity of logic","volume":"59","author":"Girard Jean-Yves","year":"1993","unstructured":"Jean-Yves Girard. 1993. On the unity of logic. Ann. Pure Appl. Logic 59, 3 (1993), 201\u2013217.","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_3_3_53_2","first-page":"1","article-title":"Linear logic: Its syntax and semantics","author":"Girard Jean-Yves","year":"1995","unstructured":"Jean-Yves Girard. 1995. Linear logic: Its syntax and semantics. London Math. Societ. Lect. Note Series 222 (1995), 1\u201342.","journal-title":"London Math. Societ. Lect. Note Series"},{"issue":"2","key":"e_1_3_3_54_2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1006\/inco.1998.2700","article-title":"Light linear logic","volume":"143","author":"Girard Jean-Yves","year":"1998","unstructured":"Jean-Yves Girard. 1998. Light linear logic. Inf. Computat. 143, 2 (1998), 175\u2013204.","journal-title":"Inf. Computat."},{"key":"e_1_3_3_55_2","first-page":"65","article-title":"Zum Intuitionistischen Aussagenkalk\u00fcl","volume":"69","author":"G\u00f6del Kurt","year":"1932","unstructured":"Kurt G\u00f6del. 1932. Zum Intuitionistischen Aussagenkalk\u00fcl. Anz. Akad. Wiss. Wien, Math. naturwiss. Kl. 69 (1932), 65\u201366.","journal-title":"Anz. Akad. Wiss. Wien, Math. naturwiss. Kl."},{"issue":"3","key":"e_1_3_3_56_2","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1093\/jigpal\/6.3.451","article-title":"Substructural logics on display","volume":"6","author":"Gor\u00e9 Rajeev","year":"1998","unstructured":"Rajeev Gor\u00e9. 1998. Substructural logics on display. Logic J. IGPL 6, 3 (1998), 451\u2013504.","journal-title":"Logic J. IGPL"},{"key":"e_1_3_3_57_2","series-title":"(Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/10722086_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Gor\u00e9 Rajeev","year":"2000","unstructured":"Rajeev Gor\u00e9. 2000. Dual intuitionistic logic revisited. In Automated Reasoning with Analytic Tableaux and Related Methods(Lecture Notes in Computer Science, Vol. 1847). Springer, 252\u2013267."},{"key":"e_1_3_3_58_2","series-title":"8th Indian Conference on Logic and its Applications (ICLA\u201919)","first-page":"144","volume":"11600","author":"Greco Giuseppe","year":"2019","unstructured":"Giuseppe Greco, Peter Jipsen, Krishna Manoorkar, Alessandra Palmigiano, and Apostolos Tzimoulis. 2019. Logics for rough concept analysis. In 8th Indian Conference on Logic and its Applications (ICLA\u201919)(LNCS, Vol. 11600). Springer, 144\u2013159."},{"key":"e_1_3_3_59_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-642-40948-6_11","volume-title":"4th International Workshop on Logic, Rationality and Interaction (LORI\u201913)","author":"Greco Giuseppe","year":"2013","unstructured":"Giuseppe Greco, Alexander Kurz, and Alessandra Palmigiano. 2013. Dynamic epistemic logic displayed. In 4th International Workshop on Logic, Rationality and Interaction (LORI\u201913)(LNCS, Vol. 8196). Springer, Berlin, 135\u2013148."},{"key":"e_1_3_3_60_2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.entcs.2019.07.007","article-title":"Proper multi-type display calculi for rough algebras","volume":"344","author":"Greco Giuseppe","year":"2019","unstructured":"Giuseppe Greco, Fei Liang, Krishna B. Manoorkar, and Alessandra Palmigiano. 2019. Proper multi-type display calculi for rough algebras. Electron. Notes Theoret. Comput. Sci. 344 (2019), 101\u2013118.","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"e_1_3_3_61_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-662-55386-2_14","volume-title":"24th International Workshop on Logic, Language, Information, and Computation","author":"Greco Giuseppe","year":"2017","unstructured":"Giuseppe Greco, Fei Liang, M. Andrew Moshier, and Alessandra Palmigiano. 2017. Multi-type display calculus for semi De Morgan logic. In 24th International Workshop on Logic, Language, Information, and Computation(LNCS, Vol. 10388). Springer, Berlin, 199\u2013215."},{"issue":"1","key":"e_1_3_3_62_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11225-020-09898-y","article-title":"Semi de Morgan logic properly displayed","volume":"109","author":"Greco Giuseppe","year":"2021","unstructured":"Giuseppe Greco, Fei Liang, M. Andrew Moshier, and Alessandra Palmigiano. 2021. Semi de Morgan logic properly displayed. Studia Logica 109, 1 (2021), 1\u201345.","journal-title":"Studia Logica"},{"key":"e_1_3_3_63_2","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1016\/j.fss.2018.05.007","article-title":"Bilattice logic properly displayed","volume":"363","author":"Greco Giuseppe","year":"2019","unstructured":"Giuseppe Greco, Fei Liang, Alessandra Palmigiano, and Umberto Rivieccio. 2019. Bilattice logic properly displayed. Fuzzy Sets Syst. 363 (2019), 138\u2013155.","journal-title":"Fuzzy Sets Syst."},{"issue":"7","key":"e_1_3_3_64_2","first-page":"1367","article-title":"Unified correspondence as a proof-theoretic tool","volume":"28","author":"Greco Giuseppe","year":"2018","unstructured":"Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Apostolos Tzimoulis, and Zhiguang Zhao. 2018. Unified correspondence as a proof-theoretic tool. J. Logic Computat. 28, 7 (2018), 1367\u20131442.","journal-title":"J. Logic Computat."},{"key":"e_1_3_3_65_2","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-3-662-55386-2_11","volume-title":"Logic, Language, Information, and Computation","author":"Greco Giuseppe","year":"2017","unstructured":"Giuseppe Greco and Alessandra Palmigiano. 2017. Lattice logic properly displayed. In Logic, Language, Information, and Computation. Springer, Berlin, 153\u2013169."},{"key":"e_1_3_3_66_2","volume-title":"Samson Abramsky on Logic and Structure in Computer Science and Beyond","author":"Greco Giuseppe","year":"2023","unstructured":"Giuseppe Greco, Valentin D. Richard, Michael Moortgat, and Apostolos Tzimoulis. 2023. Lambek-Grishin calculus: Focusing, display and full polarization. In Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Nature Switzerland AG."},{"key":"e_1_3_3_67_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5300-3","volume-title":"Metamathematics of Fuzzy Logic","author":"H\u00e1jek Petr","year":"1998","unstructured":"Petr H\u00e1jek. 1998. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers."},{"issue":"2","key":"e_1_3_3_68_2","first-page":"248","article-title":"Equational classes of relative Stone algebras","volume":"13","author":"Hecht T.","year":"1972","unstructured":"T. Hecht and Tibor Katrin\u00e1k. 1972. Equational classes of relative Stone algebras. Notre Dame J. Form. Logic 13, 2 (1972), 248\u2013254.","journal-title":"Notre Dame J. Form. Logic"},{"issue":"1","key":"e_1_3_3_69_2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0168-0072(94)90020-5","article-title":"Semantics of weakening and contraction","volume":"69","author":"Jacobs Bart","year":"1994","unstructured":"Bart Jacobs. 1994. Semantics of weakening and contraction. Ann. Pure Appl. Logic 69, 1 (1994), 73\u2013106.","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_3_3_70_2","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-94-017-2798-3_7","volume-title":"Proof Theory of Modal Logic","author":"Kracht Marcus","year":"1996","unstructured":"Marcus Kracht. 1996. Power and weakness of the modal display calculus. In Proof Theory of Modal Logic. Kluwer, 93\u2013121."},{"key":"e_1_3_3_71_2","first-page":"75","volume-title":"Specifying Syntactic Structures (Amsterdam, 1994) (Studies in Logic, Language and Information)","author":"Kurtonina Natasha","year":"1997","unstructured":"Natasha Kurtonina and Michael Moortgat. 1997. Structural control. In Specifying Syntactic Structures (Amsterdam, 1994) (Studies in Logic, Language and Information). CSLI, Stanford, CA, 75\u2013113."},{"issue":"1","key":"e_1_3_3_72_2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","article-title":"Soft linear logic and polynomial time","volume":"318","author":"Lafont Yves","year":"2004","unstructured":"Yves Lafont. 2004. Soft linear logic and polynomial time. Theoret. Comput. Sci. 318, 1 (2004), 163\u2013180.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_3_73_2","series-title":"Structure of Language and its Mathematical Aspects","first-page":"166","author":"Lambek Joachim","year":"1961","unstructured":"Joachim Lambek. 1961. On the calculus of syntactic types. In Structure of Language and its Mathematical Aspects. (Proceedings of Symposia in Applied Mathematics, Vol. XII). American Mathematical Society, 166\u2013178."},{"key":"e_1_3_3_74_2","volume-title":"Correspondence Theory in Many-valued Modal Logics","author":"Roux Cecelia le","year":"2016","unstructured":"Cecelia le Roux. 2016. Correspondence Theory in Many-valued Modal Logics. Master\u2019s Thesis. University of Johannesburg, South Africa."},{"key":"e_1_3_3_75_2","first-page":"1","article-title":"Categorical semantics of linear logic","volume":"27","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2009","unstructured":"Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical semantics of linear logic. Panoramas et Synth\u00e8ses 27 (2009), 1\u2013213.","journal-title":"Panoramas et Synth\u00e8ses"},{"key":"e_1_3_3_76_2","unstructured":"Gian Carlo Meloni and Luigi Santocanale. 2018. Relational Semantics for Distributive Linear Logic. manuscript."},{"key":"e_1_3_3_77_2","first-page":"259","volume-title":"Substructural Logics","author":"Ono Hiroakira","year":"1993","unstructured":"Hiroakira Ono. 1993. Semantics for substructural logics. In Substructural Logics. Oxford University Press, 259\u2013291."},{"issue":"3","key":"e_1_3_3_78_2","doi-asserted-by":"crossref","first-page":"817","DOI":"10.1093\/logcom\/exv041","article-title":"J\u00f3nsson-style canonicity for ALBA-inequalities","volume":"27","author":"Palmigiano Alessandra","year":"2017","unstructured":"Alessandra Palmigiano, Sumit Sourabh, and Zhiguang Zhao. 2017. J\u00f3nsson-style canonicity for ALBA-inequalities. J. Logic Computat. 27, 3 (2017), 817\u2013865.","journal-title":"J. Logic Computat."},{"issue":"3","key":"e_1_3_3_79_2","first-page":"775","article-title":"Sahlqvist theory for impossible worlds","volume":"27","author":"Palmigiano Alessandra","year":"2017","unstructured":"Alessandra Palmigiano, Sumit Sourabh, and Zhiguang Zhao. 2017. Sahlqvist theory for impossible worlds. J. Logic Computat. 27, 3 (2017), 775\u2013816.","journal-title":"J. Logic Computat."},{"issue":"3","key":"e_1_3_3_80_2","doi-asserted-by":"crossref","first-page":"979","DOI":"10.2307\/2586685","article-title":"Basic logic: Reflection, symmetry, visibility","volume":"65","author":"Sambin Giovanni","year":"2014","unstructured":"Giovanni Sambin, Giulia Battilotti, and Claudia Faggian. 2014. Basic logic: Reflection, symmetry, visibility. J. Symb. Logic 65, 3 (2014), 979\u20131013.","journal-title":"J. Symb. Logic"},{"key":"e_1_3_3_81_2","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/BFb0079691","volume-title":"The Syntax and Semantics of Infinitary Languages","author":"Tait William W.","year":"1968","unstructured":"William W. Tait. 1968. Normal derivability in classical logic. In The Syntax and Semantics of Infinitary Languages. Springer, 204\u2013236."},{"key":"e_1_3_3_82_2","series-title":"(CSLI Lectures Notes, no. 29)","volume-title":"Lectures on Linear Logic","author":"Troelstra Anne S.","year":"1992","unstructured":"Anne S. Troelstra. 1992. Lectures on Linear Logic(CSLI Lectures Notes, no. 29). Center for the Study of Language and Information, Stanford, CA."},{"key":"e_1_3_3_83_2","first-page":"225","volume-title":"Intuitionistic Logic","author":"Dalen Dirk Van","year":"1986","unstructured":"Dirk Van Dalen. 1986. Intuitionistic Logic. Springer Netherlands, Dordrecht, 225\u2013339."},{"issue":"3","key":"e_1_3_3_84_2","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0003-4843(82)90024-9","article-title":"On the completeness principle: A study of provability in Heyting\u2019s arithmetic","volume":"22","author":"Visser Albert","year":"1982","unstructured":"Albert Visser. 1982. On the completeness principle: A study of provability in Heyting\u2019s arithmetic. Ann. Math. Logic 22, 3 (1982), 263\u2013295.","journal-title":"Ann. Math. Logic"},{"key":"e_1_3_3_85_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1280-4","volume-title":"Displaying Modal Logic","author":"Wansing Heinrich","year":"1998","unstructured":"Heinrich Wansing. 1998. Displaying Modal Logic. Kluwer."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3570919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3570919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:12Z","timestamp":1750182552000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3570919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,28]]},"references-count":84,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3570919"],"URL":"https:\/\/doi.org\/10.1145\/3570919","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,1,28]]},"assertion":[{"value":"2021-12-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-26","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}