Department of Information Technology

A Verified and Executable SLR parser generator in HOL4


Aditi Barthwal

Date and Time

Tuesday, September 21st, 2010 at 10:30


Polacksbacken, room 1145


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.

Back to the seminar page

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

Updated  2010-09-17 10:23:25 by Frédéric Haziza.