avec Peter Sewell (Computer Lab, University of Cambridge, UK)
I'll describe ongoing work on tool support for writing programming language definitions. We have a prototype tool (Ott) which takes a concise definition of a language syntax and semantics, builds a parser and pretty-printer for symbolic terms thereof, and generates LaTeX and proof assistant definitions - currently for Coq, Isabelle and HOL.
Ott is available from http://moscova.inria.fr/~zappa/software/ott
Feedback on whether the Coq (and Isabelle, and HOL) code is idiomatic will be most welcome.