University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Structurally Recursive Descent Parsing

Structurally Recursive Descent Parsing

Add 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity