Total Parser Combinators Using Mixed Induction and Coinduction

Total Parser Combinators Using Mixed Induction and Coinduction
Talk given at meeting #66 of IFIP WG2.1, Atlantic City, 2010-09-20. [pdf]

Abstract

Parser combinators provide an elegant method for implementing parsers. However, most parser combinator libraries fail to guarantee that parsing will terminate. I talked 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.

For more information, see Total Parser Combinators.