A Verified and Executable SLR parser generator in HOL4

Abstract: This talk is based on the paper "Verified, Executable Parsing" [1]. 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.

[1] Aditi Barthwal and Michael Norrish. Verified, Executable Parsing. Proceedings of ESOP, York, 2009. LNCS 5502. pp160"174.