{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:34:36Z","timestamp":1767918876757,"version":"3.49.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Convertibility checking \u2014 determining whether two lambda-terms are equal up to reductions \u2014 is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are convertible, or are not convertible, without reducing them to normal form. However, these heuristics can backfire, triggering huge amounts of unnecessary computation. This paper presents a novel convertibility-checking algorithm that relies crucially on laziness and concurrency. Laziness is used to share computations, while concurrency is used to explore multiple convertibility subproblems in parallel or via fair interleaving. Unlike heuristics-based approaches, our algorithm always finds an easy solution to the convertibility problem, if one exists. The paper describes the algorithm in process calculus style, discusses its complexity, and reports on its mechanized proof of partial correctness and its lightweight experimental evaluation.<\/jats:p>","DOI":"10.1145\/3776695","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1530-1556","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Lazy, Concurrent Convertibility Checker"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8736-3060","authenticated-orcid":false,"given":"Nathana\u00eblle","family":"Courant","sequence":"first","affiliation":[{"name":"OCamlPro, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8971-9171","authenticated-orcid":false,"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[{"name":"Coll\u00e8ge de France - PSL University, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_4"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470630"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.RTA.2012.22"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001994"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103713"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500606"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110264"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2021.9"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49254-2_4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3549822"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0014565"},{"key":"e_1_2_1_16_1","unstructured":"Andrea Condoluci. 2020. Beta-Conversion Efficiently. Ph. D. Dissertation. Universit\u00e0 di Bologna. https:\/\/amsdottorato.unibo.it\/id\/eprint\/9444\/"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354174"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_2_1_19_1","unstructured":"Nathana\u00eblle Courant. 2024. Towards an efficient and formally-verified convertibility checker. Ph. D. Dissertation. Universit\u00e9 Paris Cit\u00e9. https:\/\/hal.science\/tel-04884688"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Nathana\u00eblle Courant. 2025. Artifact for \u201cA Lazy Concurrent Convertibility Checker\u201d. https:\/\/doi.org\/10.5281\/zenodo.17347533 10.5281\/zenodo.17347533","DOI":"10.5281\/zenodo.17347533"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10990-007-9015-Z"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237784"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143172"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_1_25_1","unstructured":"Jason S. Gross. 2021. Performance Engineering of Proof-Based Software Systems at Scale. Ph. D. Dissertation. MIT EECS. https:\/\/hdl.handle.net\/1721.1\/130763"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_14"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10990-007-9018-9"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2025.27"},{"key":"e_1_2_1_31_1","volume-title":"Communicating and mobile systems \u2013 the \u03c0 -calculus","author":"Milner Robin","unstructured":"Robin Milner. 1999. Communicating and mobile systems \u2013 the \u03c0 -calculus. Cambridge University Press. isbn:978-0-521-65869-0"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(3:21)2024"},{"key":"e_1_2_1_33_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","year":"1987","unstructured":"Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall. https:\/\/simon.peytonjones.org\/slpj-book-1987\/"},{"key":"e_1_2_1_34_1","unstructured":"Rocq Development Team. 2025. The Rocq Prover Reference Manual release 9.0.0. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/index.html"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31175-9_3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_30"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-019-09540-0"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90007-0"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:00:59Z","timestamp":1767898859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776695"],"URL":"https:\/\/doi.org\/10.1145\/3776695","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}