The Coq Proof Assistant

The Ott tool, developed by Peter Sewell and Francesco Zappa Nardelli, has recently been extended to compile language definitions to a Coq representation in locally-nameless style with cofinite quantification, as popularised in Engineering Formal Metatheory by Aydemir, Charguéraud, Pierce, Pollack and Weirich. It deals with the single-binder case only.

Some examples (including STLC, Fsub, and the nu-calculus of Pitts and Stark) and the documentation are available from the ln-ott page and the project web-site.

This is related to the recent LNgen tool of Brian Aydemir and Stephanie Weirich.