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.

Conference Day
Fri 19 Jun

Displayed 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 BarowyWilliams College

YouTube lightning session video

Faster General Parsing through Context-Free Memoization
PLDI Research Papers
Grzegorz HermanJagiellonian University, Poland
Zippy LL(1) Parsing with Derivatives
PLDI Research Papers
Romain EdelmannEPFL, Switzerland, Jad HamzaEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
Debug Information Validation for Optimized Code
PLDI Research Papers
Yuanbo LiGeorgia Institute of Technology, USA, Shuo DingGeorgia Institute of Technology, USA, Qirun ZhangGeorgia Institute of Technology, USA, Davide ItalianoApple, USA
Semantic Code Search via Equational Reasoning
PLDI Research Papers
Varot PremtoonMassachusetts Institute of Technology, USA, James KoppelMassachusetts Institute of Technology, USA, Armando Solar-LezamaMassachusetts Institute of Technology, USA