# Local Lexing

 Title: Local Lexing Author: Steven Obua (steven /at/ recursivemind /dot/ com) Submission date: 2017-04-28 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. BibTeX: @article{LocalLexing-AFP, author = {Steven Obua}, title = {Local Lexing}, journal = {Archive of Formal Proofs}, month = apr, year = 2017, note = {\url{http://isa-afp.org/entries/LocalLexing.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License