{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:30:39Z","timestamp":1767929439062,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T00:00:00Z","timestamp":1570406400000},"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":[[2019,10,7]]},"DOI":"10.1145\/3354166.3354174","type":"proceedings-article","created":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T12:58:36Z","timestamp":1569329916000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Sharing Equality is Linear"],"prefix":"10.1145","author":[{"given":"Andrea","family":"Condoluci","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, University of Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beniamino","family":"Accattoli","sequence":"additional","affiliation":[{"name":"LIX, Inria & \u00c9cole Polytechnique, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio Sacerdoti","family":"Coen","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, University of Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"15th International Colloquium, Stellenbosch, South Africa","author":"Accattoli Beniamino","year":"2018","unstructured":"Beniamino Accattoli . 2018 . Proof Nets and the Linear Substitution Calculus. In Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa , October 16-19, 2018, Proceedings. 37--61. https:\/\/doi.org\/10.1007\/978-3-030-02508-3_3 10.1007\/978-3-030-02508-3_3 Beniamino Accattoli. 2018. Proof Nets and the Linear Substitution Calculus. In Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings. 37--61. https:\/\/doi.org\/10.1007\/978-3-030-02508-3_3"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131855"},{"key":"e_1_3_2_1_3_1","volume-title":"On the Relative Usefulness of Fireballs. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015","author":"Accattoli Beniamino","year":"2015","unstructured":"Beniamino Accattoli and Claudio Sacerdoti Coen . 2015 . On the Relative Usefulness of Fireballs. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015 , Kyoto, Japan , July 6-10, 2015. 141--155. https:\/\/doi.org\/10.1109\/LICS.2015.23 10.1109\/LICS.2015.23 Beniamino Accattoli and Claudio Sacerdoti Coen. 2015. On the Relative Usefulness of Fireballs. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. 141--155. https:\/\/doi.org\/10.1109\/LICS.2015.23"},{"key":"e_1_3_2_1_4_1","volume-title":"FSEN 2017","author":"Accattoli Beniamino","year":"2017","unstructured":"Beniamino Accattoli and Giulio Guerrieri . 2017 . Implementing Open Call-by-Value. In Fundamentals of Software Engineering - 7th International Conference , FSEN 2017 , Tehran, Iran , April 26-28, 2017, Revised Selected Papers. 1--19. https:\/\/doi.org\/10.1007\/978-3-319-68972-2_1 10.1007\/978-3-319-68972-2_1 Beniamino Accattoli and Giulio Guerrieri. 2017. Implementing Open Call-by-Value. In Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers. 1--19. https:\/\/doi.org\/10.1007\/978-3-319-68972-2_1"},{"key":"e_1_3_2_1_5_1","volume-title":"On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12)","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli and Ugo Dal Lago . 2012 . On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. 22--37. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.22 10.4230\/LIPIcs.RTA.2012.22 Beniamino Accattoli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12), RTA 2012, May 28-June 2, 2012, Nagoya, Japan. 22--37. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.22"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603105"},{"key":"e_1_3_2_1_7_1","volume-title":"Anatomy of LISP","author":"Allen John","unstructured":"John Allen . 1978. Anatomy of LISP . McGraw-Hill, Inc. , New York, NY, USA . John Allen. 1978. Anatomy of LISP. McGraw-Hill, Inc., New York, NY, USA."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797317263"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/241388.241390"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995","author":"Guy","year":"1995","unstructured":"Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages . In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995 , La Jolla, California, USA , June 25-28, 1995 . 226--237. https:\/\/doi.org\/10.1145\/224164.224210 10.1145\/224164.224210 Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. 226--237. https:\/\/doi.org\/10.1145\/224164.224210"},{"key":"e_1_3_2_1_12_1","volume-title":"The sharing of structure in theoremproving programs. Machine intelligence 7","author":"Boyer Robert S","year":"1972","unstructured":"Robert S Boyer and Jay S Moore . 1972. The sharing of structure in theoremproving programs. Machine intelligence 7 ( 1972 ), 101--116. Robert S Boyer and Jay S Moore. 1972. The sharing of structure in theoremproving programs. Machine intelligence 7 (1972), 101--116."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295663"},{"key":"e_1_3_2_1_14_1","volume-title":"Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013","author":"Calv\u00e8s Christophe","year":"2013","unstructured":"Christophe Calv\u00e8s . 2013 . Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013 , June 24-26, 2013, Eindhoven, The Netherlands. 143--157. https:\/\/doi.org\/10.4230\/LIPIcs.RTA. 2013.143 10.4230\/LIPIcs.RTA.2013.143 Christophe Calv\u00e8s. 2013. Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands. 143--157. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.143"},{"key":"e_1_3_2_1_15_1","volume-title":"LOPSTR 2010","author":"Calv\u00e8s Christophe","year":"2010","unstructured":"Christophe Calv\u00e8s and Maribel Fern\u00e1ndez . 2010 . The First-Order Nominal Link. In Logic-Based Program Synthesis and Transformation - 20th International Symposium , LOPSTR 2010 , Hagenberg, Austria , July 23-25, 2010, Revised Selected Papers. 234--248. https:\/\/doi.org\/10.1007\/978-3-642-20551-4_15 10.1007\/978-3-642-20551-4_15 Christophe Calv\u00e8s and Maribel Fern\u00e1ndez. 2010. The First-Order Nominal Link. In Logic-Based Program Synthesis and Transformation - 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers. 234--248. https:\/\/doi.org\/10.1007\/978-3-642-20551-4_15"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2009.10.003"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_2_1_18_1","volume-title":"Sharing Equality is Linear. arXiv e-prints (Jul","author":"Condoluci Andrea","year":"2019","unstructured":"Andrea Condoluci , Beniamino Accattoli , and Claudio Sacerdoti Coen . 2019. Sharing Equality is Linear. arXiv e-prints (Jul 2019 ). arXiv:1907.06101 Andrea Condoluci, Beniamino Accattoli, and Claudio Sacerdoti Coen. 2019. Sharing Equality is Linear. arXiv e-prints (Jul 2019). arXiv:1907.06101"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/368892.368907"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/320176.320229"},{"key":"e_1_3_2_1_21_1","volume-title":"Monocopy and associative algorithms in extended Lisp. Technical report TR 74-03","author":"Goto Eiichi","unstructured":"Eiichi Goto . 1974. Monocopy and associative algorithms in extended Lisp. Technical report TR 74-03 . University of Tokyo . Eiichi Goto. 1974. Monocopy and associative algorithms in extended Lisp. Technical report TR 74-03. University of Tokyo."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628148"},{"key":"e_1_3_2_1_23_1","volume-title":"Technical Report 0. Dept. of Computer Science, Cornell U.","author":"Hopcroft J.","year":"1971","unstructured":"J. Hopcroft and R. Karp . 1971 . A Linear Algorithm for Testing Equivalence of Finite Automata . Technical Report 0. Dept. of Computer Science, Cornell U. J. Hopcroft and R. Karp. 1971. A Linear Algorithm for Testing Equivalence of Finite Automata. Technical Report 0. Dept. of Computer Science, Cornell U."},{"key":"e_1_3_2_1_24_1","volume-title":"An Algorithm for Optimal Lambda Calculus Reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages","author":"Lamping John","year":"1990","unstructured":"John Lamping . 1990 . An Algorithm for Optimal Lambda Calculus Reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages , San Francisco, California, USA , January 1990. 16--30. https:\/\/doi.org\/10.1145\/96709.96711 10.1145\/96709.96711 John Lamping. 1990. An Algorithm for Optimal Lambda Calculus Reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990. 16--30. https:\/\/doi.org\/10.1145\/96709.96711"},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010","author":"Levy Jordi","year":"2010","unstructured":"Jordi Levy and Mateu Villaret . 2010 . An Efficient Nominal Unification Algorithm . In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010 , July 11-13, 2010, Edinburgh, Scottland, UK. 209--226. https:\/\/doi.org\/10.4230\/LIPIcs.RTA. 2010.209 10.4230\/LIPIcs.RTA.2010.209 Jordi Levy and Mateu Villaret. 2010. An Efficient Nominal Unification Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK. 209--226. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.209"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 5th International Joint Conference on Artificial Intelligence","author":"Martelli Alberto","year":"1977","unstructured":"Alberto Martelli and Ugo Montanari . 1977 . Theorem Proving with Structure Sharing and Efficient Unification . In Proceedings of the 5th International Joint Conference on Artificial Intelligence . Cambridge, MA, USA , August 22-25, 1977. 543. http:\/\/ijcai.org\/Proceedings\/77-1\/Papers\/096.pdf Alberto Martelli and Ugo Montanari. 1977. Theorem Proving with Structure Sharing and Efficient Unification. In Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, MA, USA, August 22-25, 1977. 543. http:\/\/ijcai.org\/Proceedings\/77-1\/Papers\/096.pdf"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90043-0"},{"key":"e_1_3_2_1_29_1","volume-title":"International Joint Conference CAAP\/FASE","author":"Qian Zhenyu","year":"1993","unstructured":"Zhenyu Qian . 1993 . Linear Unification of Higher-Order Patterns. In TAP-SOFT'93: Theory and Practice of Software Development , International Joint Conference CAAP\/FASE , Orsay, France , April 13-17, 1993, Proceedings. 391--405. https:\/\/doi.org\/10.1007\/3-540-56610-4_78 10.1007\/3-540-56610-4_78 Zhenyu Qian. 1993. Linear Unification of Higher-Order Patterns. In TAP-SOFT'93: Theory and Practice of Software Development, International Joint Conference CAAP\/FASE, Orsay, France, April 13-17, 1993, Proceedings. 391--405. https:\/\/doi.org\/10.1007\/3-540-56610-4_78"},{"key":"e_1_3_2_1_31_1","volume-title":"Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013","author":"Schmidt-Schau\u00df Manfred","year":"2013","unstructured":"Manfred Schmidt-Schau\u00df , Conrad Rau , and David Sabel . 2013 . Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013 , June 24-26, 2013, Eindhoven, The Netherlands. 255--270. https:\/\/doi.org\/10.4230\/LIPIcs.RTA. 2013.255 10.4230\/LIPIcs.RTA.2013.255 Manfred Schmidt-Schau\u00df, Conrad Rau, and David Sabel. 2013. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands. 255--270. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.255"},{"key":"e_1_3_2_1_32_1","volume-title":"17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G\u00f6del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings. 513--527","author":"Urban Christian","year":"2003","unstructured":"Christian Urban , Andrew M. Pitts , and Murdoch Gabbay . 2003 . Nominal Unificaiton. In Computer Science Logic , 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G\u00f6del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings. 513--527 . https:\/\/doi.org\/10.1007\/978-3-540-45220-1_41 10.1007\/978-3-540-45220-1_41 Christian Urban, Andrew M. Pitts, and Murdoch Gabbay. 2003. Nominal Unificaiton. In Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G\u00f6del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings. 513--527. https:\/\/doi.org\/10.1007\/978-3-540-45220-1_41"},{"key":"e_1_3_2_1_33_1","volume-title":"Semantics and Pragmatics of the Lambda-calculus","author":"Wadsworth C.P.","unstructured":"C.P. Wadsworth , 1971. Semantics and Pragmatics of the Lambda-calculus . University of Oxford. https :\/\/books.google.it\/books?id=kl1QIQAACAAJ C.P. Wadsworth, 1971. Semantics and Pragmatics of the Lambda-calculus. University of Oxford. https:\/\/books.google.it\/books?id=kl1QIQAACAAJ"}],"event":{"name":"PPDP '19: Principles and Practice of Programming Languages 2019","location":"Porto Portugal","acronym":"PPDP '19","sponsor":["Sony Sony Corporation"]},"container-title":["Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354174","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3354166.3354174","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:56Z","timestamp":1750203896000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354174"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,7]]},"references-count":31,"alternative-id":["10.1145\/3354166.3354174","10.1145\/3354166"],"URL":"https:\/\/doi.org\/10.1145\/3354166.3354174","relation":{},"subject":[],"published":{"date-parts":[[2019,10,7]]},"assertion":[{"value":"2019-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}