ottversion

Ott is a tool for writing definitions of programming languages and calculi

It 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 LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms.

AuthorsPeter Sewell, Francesco Zappa Nardelli and Scott Owens
LicensesBSD-3-Clause and LGPL-2.1-only
Published
Homepagehttp://www.cl.cam.ac.uk/~pes20/ott/
Issue Trackerhttps://github.com/ott-lang/ott/issues
MaintainerHannes Mehnert <hannes@mehnert.org>
Dependencies
Conflicts
Source [http] https://github.com/ott-lang/ott/archive/0.26.tar.gz
sha256=fda1380c33a661290b13241c56dd29c4e09667db738dcd68bc9b388e93137e2c
md5=8aee607f1a386b3e12b1dfe0c2cf7ca1
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/ott/ott.0.26/opam
Required by