Home
Schedule
Abstract Template
Masters Attendance
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
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. * [[%ATTACHURL%/DependentlyTypedGrammarTransformations.pdf][Presentation slides]]
