A Verified and Executable SLR parser generator in HOL4
- Date and Time
Tuesday, September 21st, 2010 at 10:30
Polacksbacken, room 1145
This talk is based on the paper "Verified, Executable Parsing" . I will describe the mechanisation of an SLR parser produced by a parser generator. I will then present the main properties proved about the parser, in particular, soundness: if the parser results in a parse tree on a given input, then the parse tree is valid with respect to the grammar, and the leaves of the parse tree match the input; completeness: if the input is in the language of the grammar then the parser constructs the correct parse tree for the input with respect to the grammar; and non-ambiguity: grammars successfully converted to SLR automata are unambiguous. We will also have a brief look at the complexity introduced when providing executable versions of the algorithms involved.
 Aditi Barthwal and Michael Norrish. Verified, Executable Parsing. Proceedings of ESOP, York, 2009. LNCS 5502. pp160"174.