SpringMeeting2011AbstractTotalParserCombinator

Total Parser Combinators Using Mixed Induction and Coinduction

Abstract:

Parser combinators provide an elegant method for implementing parsers. However, most parser combinator libraries fail to guarantee that parsing will terminate. I will talk about a library which provides such a guarantee.

The library's interface is similar to that of many other parser combinator libraries, with three main differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; another is that the interface allows many forms of left recursion; and the last is that the parser type is unusually informative.