{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:13Z","timestamp":1750220053743,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Swedish Foundation for Strategic Research","award":["FFL15-0032"],"award-info":[{"award-number":["FFL15-0032"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Traditionally, a grammar defining the syntax of a programming language is typically both context free and unambiguous. However, recent work suggests that an attractive alternative is to use ambiguous grammars,thus postponing the task of resolving the ambiguity to the end user. If all programs accepted by an ambiguous grammar can be rewritten unambiguously, then the parser for the grammar is said to be resolvably ambiguous. Guaranteeing resolvable ambiguity statically---for all programs---is hard, where previous work only solves it partially using techniques based on property-based testing. In this paper, we present the first efficient, practical, and proven correct solution to the statically resolvable ambiguity problem. Our approach introduces several key ideas, including splittable productions, operator sequences, and the concept of a grouper that works in tandem with a standard parser. We prove static resolvability using a Coq mechanization and demonstrate its efficiency and practical applicability by implementing and integrating resolvable ambiguity into an essential part of the standard OCaml parser.<\/jats:p>","DOI":"10.1145\/3571251","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1686-1712","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Statically Resolvable Ambiguity"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0669-4085","authenticated-orcid":false,"given":"Viktor","family":"Palmkvist","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4918-6582","authenticated-orcid":false,"given":"Elias","family":"Castegren","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2659-5271","authenticated-orcid":false,"given":"Philipp","family":"Haller","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8457-4105","authenticated-orcid":false,"given":"David","family":"Broman","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)90680-J"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814228.2814242"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02654-1_8"},{"key":"e_1_2_1_4_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D . Ullman . 2006 . Compilers : Principles, Techniques, and Tools (second ed.). Addison Wesley , Boston. isbn:978-0-321-48681-3 Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (second ed.). Addison Wesley, Boston. isbn:978-0-321-48681-3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_34"},{"key":"e_1_2_1_6_1","unstructured":"Bas Basten. 2011. Ambiguity Detection for Programming Language Grammars. Ph. D. Dissertation. Universiteit van Amsterdam. \t\t\t\t  Bas Basten. 2011. Ambiguity Detection for Programming Language Grammars. Ph. D. Dissertation. Universiteit van Amsterdam."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76336-9_21"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357766.3359531"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/321138.321145"},{"key":"e_1_2_1_10_1","unstructured":"Arthur Chargu\u00e9raud. 2022. The TLC Coq Library. \t\t\t\t  Arthur Chargu\u00e9raud. 2022. The TLC Coq Library."},{"volume-title":"Engineering a Compiler","author":"Cooper Keith","key":"e_1_2_1_11_1","unstructured":"Keith Cooper and Linda Torczon . 2011. Engineering a Compiler ( second ed.). Elsevier . isbn:978-0-08-091661-3 Keith Cooper and Linda Torczon. 2011. Engineering a Compiler (second ed.). Elsevier. isbn:978-0-08-091661-3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24452-0_5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58768-0_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/362007.362035"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048099"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/321172.321179"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964011"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321318"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-21545-6_18"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2021\/5\/1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-05998-9_12"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3446804.3446846"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993548"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660202"},{"key":"e_1_2_1_25_1","unstructured":"Fran\u00e7ois Pottier and Yann R\u00e9gis-Gianas. 2005. The Menhir Parser Generator. \t\t\t\t  Fran\u00e7ois Pottier and Yann R\u00e9gis-Gianas. 2005. The Menhir Parser Generator."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_60"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.041"},{"volume-title":"Languages and Machines: An Introduction to the Theory of Computer Science","author":"Sudkamp Thomas A.","key":"e_1_2_1_28_1","unstructured":"Thomas A. Sudkamp . 1997. Languages and Machines: An Introduction to the Theory of Computer Science . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . isbn:978-0-201-82136-9 Thomas A. Sudkamp. 1997. Languages and Machines: An Introduction to the Theory of Computer Science. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA. isbn:978-0-201-82136-9"},{"key":"e_1_2_1_29_1","unstructured":"The dafny-lang community. 2022. Dafny Documentation. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef.html \t\t\t\t  The dafny-lang community. 2022. Dafny Documentation. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef.html"},{"key":"e_1_2_1_30_1","unstructured":"Adam Brooks Webber. 2003. Modern Programming Languages: A Practical Introduction. Franklin Beedle & Associates. isbn:978-1-887902-76-2 \t\t\t\t  Adam Brooks Webber. 2003. Modern Programming Languages: A Practical Introduction. Franklin Beedle & Associates. isbn:978-1-887902-76-2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571251","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571251"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571251"],"URL":"https:\/\/doi.org\/10.1145\/3571251","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}