Mutable Grammars

Worked with Dr. Andrés Goens, Siddharth Bhat, Jatin Agarwala, and Dr. Tobias Grosser to create a formalism to encode programming languages with grammars that can be modified at runtime, via e.g. C’s typedef commands or Lean4’s syntax macros.

This formalism was based on PEGs, and came with a static (sufficient) condition for totality (parsing always terminates, regardless of the input). We also provide a proof of concept by implementing this formalism in Lean4, and using it to write a parser for ANSI C and a fragment of Lean4.

Submitted at PLDI ‘24.