Search: WFRF:(Castegren Elias Doktor 1987 ) >
Statically Resolvab...
Statically Resolvable Ambiguity
-
- Palmkvist, Viktor (author)
- KTH,Programvaruteknik och datorsystem, SCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
- Castegren, Elias, Doktor, 1987- (author)
- Uppsala universitet,Datalogi,Uppsala Univ, Uppsala, Sweden.
-
- Haller, Philipp (author)
- KTH,Teoretisk datalogi, TCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
show more...
-
- Broman, David, 1977- (author)
- KTH,Programvaruteknik och datorsystem, SCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
show less...
-
(creator_code:org_t)
- 2023-01-11
- 2023
- English.
-
In: Proceedings of the ACM on Programming Languages. - : ACM Digital Library. - 2475-1421. ; 7:POPL, s. 1686-1712
- Related links:
-
https://doi.org/10.1...
-
show more...
-
https://uu.diva-port... (primary) (Raw object)
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Parsers
- Ambiguity
- Coq
- OCaml
- Datavetenskap
- Computer Science
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
To the university's database