You are here:
(02 Sep 2010,
Date: 2008-06-12 Time: 12:00 Room: BBL room 471 ----+++ Speaker: Andres Löh ----+++ Title: Terminating combinator parsers in Agda ----+++ Abstract [This is work in progress by Nils Anders Danielsson and Ulf Norell.] In the dependently typed programming language Agda, all functions are supposed to be total: they should terminate and produce a result on all inputs. For parser combinators, termination is not trivial to prove to the compiler. In this talk, I will explain how to design a parser combinator library for Agda that ensures termination of all type-correct parsers. As a consequence, left-recursive grammars written in this library are rejected at compilation time by Agda's type checker.
ore topic actions
Topic revision: r2 - 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?