Verified Lexical Analysis
Tobias Nipkow
This paper presents the development and verification of a (very simple)
lexical analyzer generator that takes a regular expression and yields a
functional lexical analyzer. The emphasis is on simplicity and executability.
The work was carried out with the help of the theorem prover Isabelle/HOL.
ps
SpringerLink
BibTeX:
@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow},
title={Verified Lexical Analysis},
booktitle={Theorem Proving in Higher Order Logics},
editor={J. Grundy and M. Newey},
publisher=Springer,series=LNCS,volume=1479,pages={1--15},year=1998,
note={Invited talk}}
The corresponding Isabelle theories.