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.
| Authors | Peter Sewell, Francesco Zappa Nardelli and Scott Owens |
|---|---|
| Licenses | BSD-3-Clause and LGPL-2.1-only |
| 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.28.tar.gz sha256=30c7613802cdd7f03eb1df1d634da3e13197e210d5697252382d29b5f03618f2 md5=42c76a821b8ba1528f6b99025cc6f2b0 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/ott/ott.0.28/opam |
