Structurally Recursive Descent Parsing

Add to your list(s) Download to your calendar using vCal

• Nils Anders Danielsson (University of Nottingham)
• Friday 20 March 2009, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.