Sökning: WFRF:(Castegren Elias Doktor 1987 ) >
Statically Resolvab...
Statically Resolvable Ambiguity
-
- Palmkvist, Viktor (författare)
- KTH,Programvaruteknik och datorsystem, SCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
- Castegren, Elias, Doktor, 1987- (författare)
- Uppsala universitet,Datalogi,Uppsala Univ, Uppsala, Sweden.
-
- Haller, Philipp (författare)
- KTH,Teoretisk datalogi, TCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
visa fler...
-
- Broman, David, 1977- (författare)
- KTH,Programvaruteknik och datorsystem, SCS,Digital Futures & EECS,KTH Royal Institute of Technology, Sweden
-
visa färre...
-
(creator_code:org_t)
- 2023-01-11
- 2023
- Engelska.
-
Ingår i: Proceedings of the ACM on Programming Languages. - : ACM Digital Library. - 2475-1421. ; 7:POPL, s. 1686-1712
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Parsers
- Ambiguity
- Coq
- OCaml
- Datavetenskap
- Computer Science
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas