TRX: A Formally Verified Parser Interpreter
Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. We are using parsin...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/686/pdf |
| _version_ | 1797268675353378816 |
|---|---|
| author | Adam Koprowski Henri Binsztok |
| author_facet | Adam Koprowski Henri Binsztok |
| author_sort | Adam Koprowski |
| collection | DOAJ |
| description | Parsing is an important problem in computer science and yet surprisingly
little attention has been devoted to its formal verification. In this paper, we
present TRX: a parser interpreter formally developed in the proof assistant
Coq, capable of producing formally correct parsers. We are using parsing
expression grammars (PEGs), a formalism essentially representing recursive
descent parsing, which we consider an attractive alternative to context-free
grammars (CFGs). From this formalization we can extract a parser for an
arbitrary PEG grammar with the warranty of total correctness, i.e., the
resulting parser is terminating and correct with respect to its grammar and the
semantics of PEGs; both properties formally proven in Coq. |
| first_indexed | 2024-04-25T01:36:15Z |
| format | Article |
| id | doaj.art-0b366b96d013465985e0ee6fc0b0ef85 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:15Z |
| publishDate | 2011-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-0b366b96d013465985e0ee6fc0b0ef852024-03-08T09:15:49ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-06-01Volume 7, Issue 210.2168/LMCS-7(2:18)2011686TRX: A Formally Verified Parser InterpreterAdam KoprowskiHenri BinsztokParsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. We are using parsing expression grammars (PEGs), a formalism essentially representing recursive descent parsing, which we consider an attractive alternative to context-free grammars (CFGs). From this formalization we can extract a parser for an arbitrary PEG grammar with the warranty of total correctness, i.e., the resulting parser is terminating and correct with respect to its grammar and the semantics of PEGs; both properties formally proven in Coq.https://lmcs.episciences.org/686/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theorycomputer science - programming languagesd.3.4, d.2.4, f.3.1, f.4.2 |
| spellingShingle | Adam Koprowski Henri Binsztok TRX: A Formally Verified Parser Interpreter Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory computer science - programming languages d.3.4, d.2.4, f.3.1, f.4.2 |
| title | TRX: A Formally Verified Parser Interpreter |
| title_full | TRX: A Formally Verified Parser Interpreter |
| title_fullStr | TRX: A Formally Verified Parser Interpreter |
| title_full_unstemmed | TRX: A Formally Verified Parser Interpreter |
| title_short | TRX: A Formally Verified Parser Interpreter |
| title_sort | trx a formally verified parser interpreter |
| topic | computer science - logic in computer science computer science - formal languages and automata theory computer science - programming languages d.3.4, d.2.4, f.3.1, f.4.2 |
| url | https://lmcs.episciences.org/686/pdf |
| work_keys_str_mv | AT adamkoprowski trxaformallyverifiedparserinterpreter AT henribinsztok trxaformallyverifiedparserinterpreter |