### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bååth Sjöblom, T. (2013) *An Agda proof of the correctness of Valiant’s algorithm for context free parsing*. Göteborg : Chalmers University of Technology

** BibTeX **

@mastersthesis{

Bååth Sjöblom2013,

author={Bååth Sjöblom, Thomas},

title={An Agda proof of the correctness of Valiant’s algorithm for context free parsing},

abstract={Parsing is an important problem with applications ranging from compilers to bioinformatics.
To perform the parsing more quickly, it would be desirable to be able to parse
in parallel. Valiant’s algorithm [Valiant, 1975] is a divide and conquer algorithm for
parsing and can be used to perform a large part of the work in parallel. It is fairly easy
to implement in a functional programming languages, using pattern matching. Agda is
a dependently typed functional programming language that doubles as a proof assistant
and is hence very suitable for implementing and proving the correctness of Valiant’s
algorithm.
In this thesis, we provide a very natural specification for the parsing problem and
prove that it is equivalent to the specification of the transitive closure used in [Valiant,
1975], that is further removed from both parsing and proving. We compare the two
specifications and use our specification to derive Valiant’s algorithm. We then implement
it in Agda and prove our implementation correct (we prove that it satisfies our
specification).
We also give short introductions to parsing, programming and proving with Agda
and to using algebraic structures in Agda.},

publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},

place={Göteborg},

year={2013},

keywords={Dependently typed programming, Formal proof, Agda, Valiant, Parallel parsing, Transitive closure, Nonassociative multiplication, Algebra},

note={71},

}

** RefWorks **

RT Generic

SR Electronic

ID 185016

A1 Bååth Sjöblom, Thomas

T1 An Agda proof of the correctness of Valiant’s algorithm for context free parsing

YR 2013

AB Parsing is an important problem with applications ranging from compilers to bioinformatics.
To perform the parsing more quickly, it would be desirable to be able to parse
in parallel. Valiant’s algorithm [Valiant, 1975] is a divide and conquer algorithm for
parsing and can be used to perform a large part of the work in parallel. It is fairly easy
to implement in a functional programming languages, using pattern matching. Agda is
a dependently typed functional programming language that doubles as a proof assistant
and is hence very suitable for implementing and proving the correctness of Valiant’s
algorithm.
In this thesis, we provide a very natural specification for the parsing problem and
prove that it is equivalent to the specification of the transitive closure used in [Valiant,
1975], that is further removed from both parsing and proving. We compare the two
specifications and use our specification to derive Valiant’s algorithm. We then implement
it in Agda and prove our implementation correct (we prove that it satisfies our
specification).
We also give short introductions to parsing, programming and proving with Agda
and to using algebraic structures in Agda.

PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/185016/185016.pdf

OL 30