package ott

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

Install

Dune Dependency

www.cl.cam.ac.uk Edit opam file Versions (11)

Authors

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

Maintainers

  1. H
    Hannes Mehnert <hannes@mehnert.org>

Sources

0.29.tar.gz
md5=6284382d02bd01ed00fe0e09fe3b777f

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: 02 Aug 2019

Dependencies (1)

  1. ocaml >= "4.02.0" & < "5.0"

Dev Dependencies

None

Used by (3)

  1. asli
  2. libsail
  3. sail < "0.15"

Conflicts (1)

  1. pprint >= "20220103"