Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2011/12 / Oberseminar / Andres Löh, Dependently Typed Grammars


Andres Löh, Dependently Typed Grammars

TCS Oberseminar, 04.11.2011, 14:15
Wann 14:15 15:15 04.11.2011
von bis
Wo L109
Termin übernehmen vCal
Dependently typed grammars
(Andres Löh, Well-Typed LLP)

Parser combinators are a success story for functional programming. Higher-order
functions make it incredibly easy to combine powerful parsers out of a few
small building blocks. In practice, however, parser combinators often suffer a
number of disadvantages, from the inability to handle left-recursion to
(comparatively) bad performance.

If we do not aim to describe a parser directly, but instead describe a grammar
with attached semantic functions, then we have new possibilities: We can
analyze and transform the grammar, and generate not only combinator parsers,
but also visualizations, or even perform the computations typically done by
parser generators. The challenge is to do all of this without sacrificing type
safety, and maintaining the benefits and flexibility of parser combinators.

In this talk, I will demonstrate that in a dependently typed programming
language such as Agda, we can get quite close to that goal.


abgelegt unter: