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

Semantic definitions of full-scale programming languages are rarely
given, 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, and Isabelle/HOL, 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 (OCaml_{light}, 310 rules), with mechanised 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.