Dependently Typed Grammar Transformations
Stc
Date: 2009-05-28
Time: 11:45
Room: BBL room 471
Speaker: Kasper Brink
Title: Dependently Typed Grammar Transformations (thesis defense)
Abstract
Parser Combinators form an elegant way to implement parsers in a functional
language. In this formalism, a parser is a directly executable
specification of a grammar. Unfortunately, because a parser is a function,
it is not possible to analyze and transform the underlying grammar.
To solve this problem, we have developed a grammar library in the
dependently typed language Agda. We represent a grammar as a value of a
datatype, so that it can be inspected and transformed before constructing
the parser. Using the library, we have implemented the left-corner grammar
transform, which removes left-recursion from a grammar. Agda's dependent
type system plays an important role in specifying the types of the semantic
functions of the grammar, and the way in which these types are transformed.
Agda is not only a dependently typed programming language, but also a proof
assistant for constructive logic. This enables us to develop a correctness
proof for our implementation of the left-corner transform. Finally, we
compare our approach to the work of Arthur Baars, Doaitse Swierstra, and
Marcos Viera, who have implemented the typed left-corner transform in
Haskell.
