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: 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

06:20 - 06:40
Talk
Faster General Parsing through Context-Free Memoization
PLDI Research Papers
Grzegorz HermanJagiellonian University, Poland
06:40 - 07:00
Talk
Zippy LL(1) Parsing with Derivatives
PLDI Research Papers
Romain EdelmannEPFL, Switzerland, Jad HamzaEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
07:00 - 07:20
Talk
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
07:20 - 07:40
Talk
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