Title: An Algebraic Regular Parser Generator

Speaker: Greg Morrisett (Harvard University)

Time: 15:30, 22nd April 2014

Venue: Lecture Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

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.

Biography:

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