Opam Package ott.0.30

Package info

opam-nameott
opam-version0.30
synopsisA 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.
authors
  • Peter Sewell
  • Francesco Zappa Nardelli
  • Scott Owens
homepagehttp://www.cl.cam.ac.uk/~pes20/ott/
licensepart BSD3, part LGPL 2.1
deps (1)
revdeps (2)
metas(0)
libraries(0)

Package modules

Package sources

ott

Package files

share/tex/ottlayout.sty
share/tex
share/ott/menhir_library_extra.mly
share/ott
share/emacs/site-lisp/ott-mode.el
doc/ott/doc/ott_manual.pdf
doc/ott/doc/ott_manual.html
doc/ott/doc
doc/ott
bin/ott