LL(1) Parser Generator

Sarah Tilscher 📧 and Simon Wimmer 📧

May 2, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In this formalization, we implement an LL(1) parser generator that first pre-computes the NULLABLE set, FIRST map and FOLLOW map, to then build a lookahead table. We prove correctness, soundness and error-free termination for LL(1) grammars. We provide the JSON grammar and show how to parse a tokenized JSON string using a parser created with the verified parser generator. The proof structure is significantly based on Vermillion, an LL(1) parser generator verified in Coq.


BSD License


Session LL1_Parser