ott
Authors | { Peter Sewell, Francesco Zappa Nardelli, Scott Owens } |
---|---|
License | part BSD3, part LGPL 2.1 |
Homepage | http://www.cl.cam.ac.uk/~pes20/ott/ |
Issue Tracker | https://github.com/ott-lang/ott/issues |
Maintainer | Hannes Mehnert <hannes@mehnert.org> |
Published | Oct 5, 2014 |
Source [http] |
http://github.com/ott-lang/ott/archive/0.25.tar.gz 2b888fee23b1aa4537f5bd638d502664 |
Statistics | Installed 13 times in last month. |
Edit | https://github.com/ocaml/opam-repository/tree/master/packages/ott/ott.0.25/opam |
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.
No package is dependent |