University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > A Verifiable, Executable SLR Parser

A Verifiable, Executable SLR Parser

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk.

This talk is based on one I will be presenting at the ESOP conference. In this talk, I will describe the mechanisation of an SLR parser produced by a parser generator. I will 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 briefly have a look at the complexity introduced when providing executable versions of the algorithms involved.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity