An Algebraic Regular Parser Generator
Most tools for reasoning about programs start with abstract syntax trees (ASTs), but many flaws we find in systems arise within concrete syntax (c.f., SQL injection attacks). In this talk, I will describe some on-going work using Coq to construct efficient, provably correct parsers from regular grammars. The approach is based on a generalization of the algebraic techniques of Brzozowski, and leads to an elegant theory that is surprisingly tricky to formalize.
Greg Morrisett is Allen B. Cutting Professor of Computer Science at Harvard University (Cambridge, USA). He is an expert in Programming Languages and Verification of Software systems. More information is available at www.eecs.harvard.edu/~greg .