### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Programming languages/Compiling

### Session LL1_Parser

- Grammar
- Nullable_Set
- First_Map
- Follow_Map
- Parse_Table
- LL1_Parser
- LL1_Parser_show
- Parser_Example
- Json_Parser

### Depends on

- Haskell’s Show Class in Isabelle/HOL

## Cite

×

LL1_Parser-AFP

    @article{LL1_Parser-AFP,
      author  = {Sarah Tilscher and Simon Wimmer},
      title   = {LL(1) Parser Generator},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/LL1_Parser.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest