ott

A tool for writing definitions of programming languages and calculi
Description

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.
Install
Sources
0.32.tar.gz
md5=f36d94978be65d7837fe4a1c24672d2e
sha512=f38e12c079426c5a460a9ab24e58f098410ceb5ae0284c1719c50f6d7cd88f6b9c4da6beb5425c03f2dc056c7a9cb597f9bf2983abb525e3c003e45858496ad3
Dependencies
menhir
>= "20151112" & with-test
pprint
with-test
ocamlfind
with-test
ocamlbuild
with-test
ocaml
>= "4.02.0"
Reverse Dependencies