Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020

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 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

06:20 - 07:40: PLDI Research Papers - Parsing, Debugging, and Code Search at PLDI Research Papers live stream
Chair(s): Dan BarowyWilliams College

YouTube lightning session video

pldi-2020-papers06:20 - 06:40
Grzegorz HermanJagiellonian University, Poland
pldi-2020-papers06:40 - 07:00
Romain EdelmannEPFL, Switzerland, Jad HamzaEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
pldi-2020-papers07:00 - 07:20
Yuanbo LiGeorgia Institute of Technology, USA, Shuo DingGeorgia Institute of Technology, USA, Qirun ZhangGeorgia Institute of Technology, USA, Davide ItalianoApple, USA
pldi-2020-papers07:20 - 07:40
Varot PremtoonMassachusetts Institute of Technology, USA, James KoppelMassachusetts Institute of Technology, USA, Armando Solar-LezamaMassachusetts Institute of Technology, USA