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{https://isa-afp.org/entries/LocalLexing.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.