Ott: Effective tool support for the working semanticist

Peter Sewell*, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


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 U 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.

Original languageEnglish
Pages (from-to)1-12
Number of pages12
JournalACM SIGPLAN Notices
Issue number9
Publication statusPublished - Sept 2007
Event12th ACM SIGPLAN International Conference on Functional Programming - Freiburg, Germany
Duration: 1 Oct 20073 Oct 2007


  • languages
  • verification
  • theory
  • standardization


Dive into the research topics of 'Ott: Effective tool support for the working semanticist'. Together they form a unique fingerprint.

Cite this