Dependently Typed Grammars

10 years 2 months ago
Dependently Typed Grammars
Parser combinators are a popular tool for designing parsers in functional programming languages. If such combinators generate an abstract representation of the grammar as an intermediate step, it becomes easier to perform analyses and transformations that can improve the behaviour of the resulting parser. Grammar transformations must satisfy a number of invariants. In particular, they have to preserve the semantics associated with the grammar. Using conventional type systems, these constraints cannot be expressed satisfactorily, but as we show in this article, dependent types are a natural fit. We present a framework for grammars and grammar transformations using Agda. We implement the left-corner transformation for left-recursion removal and prove a language-inclusion property as use cases. Key words: context-free grammars, grammar transformation, dependently typed programming
Kasper Brink, Stefan Holdermans, Andres Löh
Added 20 Jul 2010
Updated 20 Jul 2010
Type Conference
Year 2010
Where MPC
Authors Kasper Brink, Stefan Holdermans, Andres Löh
Comments (0)