Abstract
This formalisation accompanies the paper Local
Lexing which introduces a novel parsing concept of the same
name. The paper also gives a high-level algorithm for local lexing as
an extension of Earley's algorithm. This formalisation proves the
algorithm to be correct with respect to its local lexing semantics. As
a special case, this formalisation thus also contains a proof of the
correctness of Earley's algorithm. The paper contains a short
outline of how this formalisation is organised.
BSD License