Local Lexing

Steven Obua 📧

April 28, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Topics

Theories of LocalLexing