Terminating Combinator Parsers In Agda
Stc
Date: 2008-06-12
Time: 12:00
Room: BBL room 471
Speaker: Andres Löh
Title: Terminating combinator parsers in Agda
Abstract
[This is work in progress by Nils Anders Danielsson and Ulf Norell.]
In the dependently typed programming language Agda, all functions are
supposed to be total: they should terminate and produce a result on all
inputs. For parser combinators, termination is not trivial to prove to
the compiler. In this talk, I will explain how to design a parser
combinator library for Agda that ensures termination of all type-correct
parsers. As a consequence, left-recursive grammars written in this
library are rejected at compilation time by Agda's type checker.
