####
Ott: Effective Tool Support for the Working Semanticist

It is rare to give a semantic definition of a full-scale programming
language, despite the many potential benefits. Partly this is because
the available *metalanguages* for expressing semantics ---
usually either LaTeX for informal mathematics, or the formal
mathematics of a proof assistant --- make it much harder than
necessary to work with large definitions.

We present a metalanguage specifically designed for this problem, and
a tool, `ott`, that sanity-checks such definitions and compiles
them into proof assistant code for Coq, HOL, Isabelle, and (in
progress) Twelf, together with LaTeX code for production-quality
typesetting, and OCaml boilerplate. The main innovations are:
(1) metalanguage design to make definitions concise, and easy to read and edit;
(2) an expressive but intuitive metalanguage for specifying binding structures; and
(3) compilation to proof assistant code.

This has been tested in substantial case studies, including modular
specifications of calculi from the TAPL text, a Lightweight Java with
Java JSR 277/294 module system proposals, and a large fragment of
OCaml (around 306 rules), with machine proofs of various soundness
results. Our aim with this work is to enable a phase change: making
it feasible to work routinely, without heroic effort, with rigorous
semantic definitions of realistic languages.