ott

Ott is a tool for writing definitions of programming languages and calculi
Description

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.

Install
Documentation www.cl.cam.ac.uk Edit opam file
Published
25 Apr 2018
Authors
Maintainers
Sources
0.28.tar.gz
md5=42c76a821b8ba1528f6b99025cc6f2b0
Dependencies
ocaml >= "4.00.0" & < "5.0"
Reverse Dependencies
asli
libsail
sail < "0.15"
Conflicts
pprint >= "20220103"