BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Structurally Recursive Descent Parsing - Nils Anders Danielsson (U
 niversity of Nottingham)
DTSTART:20090320T140000Z
DTEND:20090320T150000Z
UID:TALK17283@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Parser combinators provide an elegant method for writing execu
 table specifications of grammars. Implementations of parser combinators us
 ing recursive descent have a problem\, though: if the specified grammar is
  left recursive\, then parsing fails to terminate.\n\nWe address this prob
 lem by defining a type of grammars without left recursion. The type is def
 ined 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 posi
 tions where a token will have been consumed. Parsing can then be implement
 ed using recursion over the structure of a grammar's inductive part and a 
 bound on the input string's length.\n\nOn top of this type we have impleme
 nted a library of parser combinators which retains much of the flavour of 
 ordinary "list of successes" combinator parsers. The library is implemente
 d in the total dependently typed functional language Agda.\n\nThis is join
 t work with Ulf Norell.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR