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.
| Authors | Peter Sewell, Francesco Zappa Nardelli and Scott Owens |
|---|---|
| License | part BSD3, part LGPL 2.1 |
| Published | |
| Homepage | http://www.cl.cam.ac.uk/~pes20/ott/ |
| Issue Tracker | https://github.com/ott-lang/ott/issues |
| Maintainer | Hannes Mehnert <hannes@mehnert.org> |
| Dependencies |
|
| Conflicts |
|
| Source [http] | https://github.com/ott-lang/ott/archive/0.31.tar.gz md5=ef699aa19323e54c205babe17b5489ff sha512=d885ac3e7d835705342f476200bcbbdc278bcf44418d5365f02b4e92e4d630d6d080bfb008e6742fc3354de3379a99afc5263b66a612a9ac4ce20231f4500f4a |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/ott/ott.0.31/opam |
