ott
  1. Overview
  2. Docs
A tool for writing definitions of programming languages and calculi

Install

www.cl.cam.ac.uk Readme BSD-3-Clause; LGPL-2.1-only License Edit opam file

Authors

  1. P
    Peter Sewell
  2. F
    Francesco Zappa Nardelli
  3. S
    Scott Owens

Maintainers

  1. T
    Thibaut Pérami <Thibaut.Perami@cl.cam.ac.uk>

Sources

0.33.tar.gz
sha512=fd601ef958e52ca461eaff8175323416e3e524e1ba11fcf5328827ef2cb9ee3d54111843adb54d3c32e2f08c7c70214558bf5519fb8385bfa58049f22237c3c6

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.

Published: 18 Jan 2023

Dependencies (2)

  1. ocamlgraph
  2. ocaml >= "4.07.0"

Dev Dependencies (4)

  1. menhir >= "20151112" & with-test
  2. pprint with-test
  3. ocamlfind build | with-test
  4. ocamlbuild with-test

Used by (2)

  1. libsail
  2. sail < "0.15"

Conflicts

None