@inproceedings{EdelmannZippy2020,
 title = {Zippy LL(1) parsing with derivatives},
 author = {Edelmann, Romain and Hamza, Jad and Kun\v{c}ak, Viktor},
 year = {2020},
 isbn = {9781450376136},
 doi = {10.1145/3385412.3385992},
 url = {https://doi.org/10.1145/3385412.3385992},
 booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI 2020},
 pages = {1036–1051},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 location = {London, UK},
 keywords = {Zipper, Parsing, LL(1), Formal proof, Derivatives},
 numpages = {16},
 abstract = {In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.}
}