A tool for writing definitions of programming languages and calculi

Ott takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates output:

  • a LaTeX source file that defines commands to build a typeset version of the definition;
  • a Coq version of the definition;
  • a HOL version of the definition;
  • an Isabelle/HOL version of the definition;
  • a Lem version of the definition;
  • an OCaml version of the syntax of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by typeset terms.
AuthorsPeter Sewell, Francesco Zappa Nardelli and Scott Owens
LicensesBSD-3-Clause and LGPL-2.1-only
Issue Tracker
MaintainerThibaut PĂ©rami <>
Source [http]
Required by