formalization of operator precedence parsing

Stream: general

[Frederick Pu]

are there any formal proofs of correctness for operator precedence parsing eg of Shunting Yard algorithm anywhere. Seems like a pretty common algorithm i wonder if it's hidden in Lean4Lean or CeriCoq anywhere

[Marcus Rossel]

I’m guessing this isn’t exactly what you’re looking for, but I have started proving correctness of Shunting-Yard for a specific language as part of the human-eval-lean project. I haven‘t quite finished it, but here‘s the progress:

https://github.com/leanprover/human-eval-lean/pull/167/files#diff-ed465974152705a644b84da9042e367b0c907412e6528a2db0bb0273028c7b76