EdelmannZippy2020:
  type: article
  title: Zippy LL(1) parsing with derivatives
  author:
  - Edelmann, Romain
  - Hamza, Jad
  - Kunčak, Viktor
  date: 2020
  page-range: 1036-1051
  url: https://doi.org/10.1145/3385412.3385992
  serial-number:
    doi: 10.1145/3385412.3385992
    isbn: '9781450376136'
  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.
  parent:
    type: proceedings
    title: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
    publisher:
      name: Association for Computing Machinery
      location: London, UK
    parent:
      type: proceedings
      title: PLDI 2020