You are here:
(02 Sep 2010,
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. * [[%ATTACHURL%/DependentlyTypedGrammarTransformations.pdf][Presentation slides]]
ore topic actions
Topic revision: r3 - 02 Sep 2010,
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?