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.

dvi ps SpringerLink


@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow},
title={Verified Lexical Analysis},
booktitle={Theorem Proving in Higher Order Logics},
editor={J. Grundy and M. Newey},
note={Invited talk}}
The corresponding Isabelle theories.