Skip to main content


Verified, executable parsing


Aditi Barthwal and Michael Norrish

Australian National University



We describe the mechanisation of SLR parsing, covering background properties of context-free languages and grammars, as well as the construction of an SLR automaton. Among the various properties proved about the parser we show, 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 also develop versions of the algorithms that are executable by automatic translation from HOL to SML. These alternative versions of the algorithms require some interesting termination proofs.

BibTeX Entry

    publisher        = {Springer},
    author           = {Barthwal, Aditi and Norrish, Michael},
    month            = mar,
    editor           = {{Giuseppe Castagna}},
    year             = {2009},
    keywords         = {mechanisation, parsing, slr},
    title            = {Verified, Executable Parsing},
    booktitle        = {European Symposium on Programming},
    pages            = {160-174},
    address          = {York}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.