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.
Fri 19 JunDisplayed time zone: Pacific Time (US & Canada) change
06:20 - 07:40 | Parsing, Debugging, and Code SearchPLDI Research Papers at PLDI Research Papers live stream Chair(s): Dan Barowy Williams College | ||
06:20 20mTalk | Faster General Parsing through Context-Free Memoization PLDI Research Papers Grzegorz Herman Jagiellonian University, Poland | ||
06:40 20mTalk | Zippy LL(1) Parsing with Derivatives PLDI Research Papers | ||
07:00 20mTalk | Debug Information Validation for Optimized Code PLDI Research Papers Yuanbo Li Georgia Institute of Technology, USA, Shuo Ding Georgia Institute of Technology, USA, Qirun Zhang Georgia Institute of Technology, USA, Davide Italiano Apple, USA | ||
07:20 20mTalk | Semantic Code Search via Equational Reasoning PLDI Research Papers Varot Premtoon Massachusetts Institute of Technology, USA, James Koppel Massachusetts Institute of Technology, USA, Armando Solar-Lezama Massachusetts Institute of Technology, USA | ||