Install ott with Homebrew, apt, MacPorts, Nix

Project links

• Homepage
• Repository
• Upstream docs
• Package manager page

Commands and aliases

• ott

Project history

Ott was principally developed by Peter Sewell, Francesco Zappa Nardelli, and Scott Owens, with a wider contributor group. Its design was published at ICFP 2007 and then as a Journal of Functional Programming article in January 2010.

The project arose from a specific pain point in programming-language research: full-scale semantic definitions are valuable but hard to keep consistent when they live only in informal mathematics or inside a single proof assistant. Ott's answer was a readable ASCII notation plus sanity checking and code generation into both publication and mechanized-proof formats.

Adoption history

The Ott manual and repository document examples spanning untyped and simply typed lambda calculi, ML polymorphism, POPLmark F<:, TAPL systems, a Leroy-style module system, Lightweight Java, Java module-system work, and a substantial OCaml-light semantics. The JFP paper reports larger case studies including OCaml light with 310 rules and mechanized soundness results.

Ott's adoption is strongest in programming-languages research, where the same source definition can support papers, collaborative editing, and proof assistant artifacts. The 2010 'Ott or Nott' workshop abstract is a useful adoption signal: it presents Ott as part of a working language-design process, not merely as a backend generator.

How it is used

A typical user writes an .ott source file describing object-language syntax and semantic judgments, then invokes ott with one or more -o outputs such as .tex, .v, .thy, HOL script, Lem, or OCaml files. The tool can also filter embedded terms in LaTeX, Coq, Isabelle/HOL, Lem, or OCaml source.

The generated artifacts reduce drift between the published rules, the parser-level syntax, and the formal definitions used for mechanized reasoning. For package users, the command-line binary is the bridge between a research notation and several proof and documentation ecosystems.

Why package nerds care

Ott is a rare package that is both a compiler-like CLI and a research infrastructure artifact. Its package value comes from reproducibility: a language-definition source can be checked, regenerated, versioned, and consumed by multiple proof assistants and typesetting workflows.

Timeline

• 2007: Ott was presented at ICFP as 'Effective Tool Support for the Working Semanticist'.
• 2010: The Journal of Functional Programming article expanded the Ott design, motivation, and case studies.
• 2010: 'Ott or Nott' discussed the experience of using Ott in programming-language design and mechanized-metatheory workflows.
• 2024: The GitHub README stated that Ott remained in continuous use.

Related projects

• Ott sits alongside Coq, HOL, Isabelle/HOL, Lem, OCaml, LaTeX, POPLmark, TAPL-style calculi, Lightweight Java, and OCaml-light semantics work.

Sources

• https://dl.acm.org/doi/10.1145/1291220.1291155
• https://github.com/ott-lang/ott
• https://www.cambridge.org/core/journals/journal-of-functional-programming/article/ott-effective-tool-support-for-the-working-semanticist/4F02FB206B5209D42B3BF2ED2240A802
• https://www.cis.upenn.edu/~bcpierce/wmm/wmm10/sewell.pdf
• https://www.cl.cam.ac.uk/~pes20/ott/top2.html