ottversion

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
Licensepart BSD3, part LGPL 2.1
Published
Homepagehttp://www.cl.cam.ac.uk/~pes20/ott/
Issue Trackerhttps://github.com/ott-lang/ott/issues
MaintainerHannes Mehnert <hannes@mehnert.org>
Dependencies
Source [http] https://github.com/ott-lang/ott/archive/0.31.tar.gz
md5=ef699aa19323e54c205babe17b5489ff
sha512=d885ac3e7d835705342f476200bcbbdc278bcf44418d5365f02b4e92e4d630d6d080bfb008e6742fc3354de3379a99afc5263b66a612a9ac4ce20231f4500f4a
StatisticsInstalled 1148 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/ott/ott.0.31/opam
Required by