{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:10Z","timestamp":1751663410203,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            The notion of \ud835\udefc-equivalence between \ud835\udf06-terms is commonly used to identify terms that are considered equal. However, due to the primitive treatment of free variables, this notion falls short when comparing subterms occurring within a larger context. Depending on the usage of the Barendregt convention (choosing different variable names for all involved binders), it will equate either too few or too many subterms. We introduce a formal notion of context-sensitive \ud835\udefc-equivalence, where two open terms can be compared within a context that resolves their free variables. We show that this equivalence coincides exactly with the notion of bisimulation equivalence. Furthermore, we present an efficient\n            <jats:italic toggle=\"yes\">O<\/jats:italic>\n            (\n            <jats:italic toggle=\"yes\">n<\/jats:italic>\n            log\n            <jats:italic toggle=\"yes\">n<\/jats:italic>\n            ) runtime hashing scheme that identifies \ud835\udf06-terms modulo context-sensitive\n            <jats:italic toggle=\"yes\">\ud835\udefc<\/jats:italic>\n            -equivalence, generalizing over traditional bisimulation partitioning algorithms and improving upon a previously established\n            <jats:italic toggle=\"yes\">O<\/jats:italic>\n            (\n            <jats:italic toggle=\"yes\">n<\/jats:italic>\n            log\n            <jats:sup>2<\/jats:sup>\n            <jats:italic toggle=\"yes\">n<\/jats:italic>\n            ) bound for a hashing modulo ordinary \ud835\udefc-equivalence byMaziarz et al [\n            <jats:xref ref-type=\"bibr\">21<\/jats:xref>\n            ]. Hashing \ud835\udf06-terms is useful in many applications that require common subterm elimination and structure sharing. We hav employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.\n          <\/jats:p>","DOI":"10.1145\/3656459","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"2027-2050","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Hashing Modulo Context-Sensitive \u03b1-Equivalence"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2910-8069","authenticated-orcid":false,"given":"Lasse","family":"Blaauwbroek","sequence":"first","affiliation":[{"name":"Institut des Hautes \u00c9tudes Scientifiques, Bures-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9361-1921","authenticated-orcid":false,"given":"Miroslav","family":"Ol\u0161\u00e1k","sequence":"additional","affiliation":[{"name":"Institut des Hautes \u00c9tudes Scientifiques, Bures-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2522-2980","authenticated-orcid":false,"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_1_2_1","DOI":"10.2168\/LMCS-12(1:4)2016"},{"unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press.","key":"e_1_3_1_3_1"},{"key":"e_1_3_1_4_1","volume-title":"Studies in logic and the foundations of mathematics, Vol. 103. Elsevier, North-Holland","author":"Barendregt Hendrik Pieter","year":"1985","unstructured":"Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, Vol. 103. Elsevier, North-Holland."},{"unstructured":"Maciej Bendkowski. 2020. How to generate random lambda terms? CoRR abs\/2005.08856 (2020). arXiv:2005.08856 https:\/\/arxiv.org\/abs\/2005.08856","key":"e_1_3_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_1_6_1","DOI":"10.1016\/j.entcs.2007.01.018"},{"doi-asserted-by":"publisher","unstructured":"Lasse Blaauwbroek. 2023. Reference Implementation for Hashing Modulo Context-Sensitive Alpha-Equivalence. https:\/\/doi.org\/10.5281\/zenodo.11097757 10.5281\/zenodo.11097757","key":"e_1_3_1_7_1","DOI":"10.5281\/zenodo.11097757"},{"doi-asserted-by":"publisher","unstructured":"Lasse Blaauwbroek. 2024. The Tactician\u2019s Web of Large-Scale Formal Knowledge. arXiv preprint (Jan. 2024). https:\/\/doi.org\/10.48550\/arXiv.2401.02950 10.48550\/arXiv.2401.02950 arXiv:2401.02950 [cs.LO]","key":"e_1_3_1_8_1","DOI":"10.48550\/arXiv.2401.02950"},{"doi-asserted-by":"publisher","key":"e_1_3_1_9_1","DOI":"10.48550\/ARXIV.2401.02948"},{"doi-asserted-by":"publisher","key":"e_1_3_1_10_1","DOI":"10.1145\/224164.224210"},{"doi-asserted-by":"publisher","unstructured":"Arthur Chargueraud. 2012. The Locally Nameless Representation. J. Autom. Reason. 49 3 (2012) 363-408. https:\/\/doi.org\/10.1007\/S10817-011-9225-2 10.1007\/S10817-011-9225-2","key":"e_1_3_1_11_1","DOI":"10.1007\/S10817-011-9225-2"},{"unstructured":"Paul Chiusano Runar Bjarnason and Arya Irani. [n. d.]. Unison: A friendly statically-typed functional programming language from the future \u00b7 UNISON programming language. https:\/\/www.unison-lang.org\/","key":"e_1_3_1_12_1"},{"key":"e_1_3_1_13_1","volume-title":"Princeton: Princeton University Press","author":"Church Alonzo","year":"1941","unstructured":"Alonzo Church. 1941. The Calculi ofLambda-Conversion. Princeton: Princeton University Press"},{"doi-asserted-by":"publisher","key":"e_1_3_1_14_1","DOI":"10.1145\/800028.808480"},{"doi-asserted-by":"publisher","key":"e_1_3_1_15_1","DOI":"10.1145\/3354166.3354174"},{"doi-asserted-by":"publisher","key":"e_1_3_1_16_1","DOI":"10.1007\/978-3-319-21401-6_26"},{"doi-asserted-by":"publisher","key":"e_1_3_1_17_1","DOI":"10.1016\/S0304-3975(03)00361-X"},{"doi-asserted-by":"publisher","key":"e_1_3_1_18_1","DOI":"10.1145\/1159876.1159880"},{"doi-asserted-by":"publisher","key":"e_1_3_1_19_1","DOI":"10.1145\/2628136.2628148"},{"doi-asserted-by":"publisher","unstructured":"Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and generating lambda terms. J. Funct. Program. 23 5 (2013) 594-628. https:\/\/doi.org\/10.1017\/S0956796813000178 10.1017\/S0956796813000178","key":"e_1_3_1_20_1","DOI":"10.1017\/S0956796813000178"},{"doi-asserted-by":"publisher","key":"e_1_3_1_21_1","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"doi-asserted-by":"publisher","key":"e_1_3_1_22_1","DOI":"10.1145\/3453483.3454088"},{"doi-asserted-by":"publisher","key":"e_1_3_1_23_1","DOI":"10.1145\/1481861.1481862"},{"doi-asserted-by":"publisher","key":"e_1_3_1_24_1","DOI":"10.1137\/0216062"},{"doi-asserted-by":"publisher","key":"e_1_3_1_25_1","DOI":"10.48550\/arXiv.2401.02949"},{"doi-asserted-by":"publisher","key":"e_1_3_1_26_1","DOI":"10.1145\/289423.289460"},{"doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2020. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.4021912 10.5281\/zenodo.4021912","key":"e_1_3_1_27_1","DOI":"10.5281\/zenodo.4021912"},{"doi-asserted-by":"publisher","key":"e_1_3_1_28_1","DOI":"10.1109\/IWSC.2012.6227862"},{"doi-asserted-by":"publisher","key":"e_1_3_1_29_1","DOI":"10.1016\/J.IPL.2011.12.004"},{"doi-asserted-by":"publisher","key":"e_1_3_1_30_1","DOI":"10.1109\/BWCCA.2015.52"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656459","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656459","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:43Z","timestamp":1751661703000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656459"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":29,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656459"],"URL":"https:\/\/doi.org\/10.1145\/3656459","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}