TY - GEN
T1 - Verified, executable parsing
AU - Barthwal, Aditi
AU - Norrish, Michael
PY - 2009
Y1 - 2009
N2 - We describe the mechanisation of an SLR parser produced by a parser generator, 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.
AB - We describe the mechanisation of an SLR parser produced by a parser generator, 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.
UR - http://www.scopus.com/inward/record.url?scp=67650134650&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-00590-9_12
DO - 10.1007/978-3-642-00590-9_12
M3 - Conference contribution
SN - 9783642005893
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 160
EP - 174
BT - Programming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings
T2 - 18th European Symposium on Programming, ESOP 2009
Y2 - 22 March 2009 through 29 March 2009
ER -