![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Structurally Recursive Descent Parsing
Structurally Recursive Descent ParsingAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Sam Staton. Parser combinators provide an elegant method for writing executable specifications of grammars. Implementations of parser combinators using recursive descent have a problem, though: if the specified grammar is left recursive, then parsing fails to terminate. We address this problem by defining a type of grammars without left recursion. The type is defined using a mixture of induction and coinduction, in order to avoid left recursion (induction) but still allow the definition of cyclic grammars (coinduction). Dependent types ensure that coinduction is only used in positions where a token will have been consumed. Parsing can then be implemented using recursion over the structure of a grammar’s inductive part and a bound on the input string’s length. On top of this type we have implemented a library of parser combinators which retains much of the flavour of ordinary “list of successes” combinator parsers. The library is implemented in the total dependently typed functional language Agda. This is joint work with Ulf Norell. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsMeasuring National Well-Being – what matters to you? Cambridge Institute for Sustainability Leadership DPMMS ListsOther talksSouth American Opuntioids Statistical analysis of biotherapeutic datasets to facilitate early ‘Critical Quality Attribute’ characterization. The Most Influential Living Philosopher? Recent Advances in Solid State Batteries and Beyond Li Technologies - Challenges for Fundamental Science The Move of Economics Ideas and Numbers into Policy The persistence and transience of memory |