Institute of Cybernetics at TUT
Thursday, 19 January 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Parsing is a fundamental component of many software pieces. The ultimate goal of our project is to implement a parser generator for context-free languages, which, given a context-free grammar, should be able to provide a parser together with an independently checkable certificate of its correctness.
As a first approximation of our main goal, we implemented a parser generator for regular languages and showed its correctness using the Agda programming language. Specifically, we programmed a transformation of regular expressions into a Boolean-matrix based representation of finite automata. And we proved (in Agda) that a string matches a regular expression if and only if the finite automaton accepts it.