← All repos

ott

The Ott tool for writing definitions of programming languages and calculi

GitHub
Browse cluster: OCaml Systems and Utilities →
367commits
30contributors
11languages

Tech stack & purpose

Ott is a tool for writing formal definitions of programming languages and calculi. It accepts concise, readable ASCII notation describing language syntax and semantics, then generates output in multiple formats: LaTeX for typeset definitions, and formal specifications for Coq, HOL, Isabelle/HOL, Lem, and OCaml, along with experimental support for Menhir parsers. The tool can also function as a filter to parse and replace embedded language terms in LaTeX or proof assistant source files. Ott is implemented in OCaml and depends on the ocamlgraph library. The project has been principally developed by Peter Sewell, Francesco Zappa Nardelli, and Scott Owens at the University of Cambridge and INRIA, with contributions from numerous researchers. The distribution includes substantial examples, most notably a formal specification of OCaml's core language by Scott Owens and colleagues.

Community & reference links

Languages

OCaml
61.7%
HTML
29.0%
Rocq Prover
3.1%
Makefile
1.8%
TeX
1.5%
Awk
1.4%
Standard ML
0.8%
Isabelle
0.4%
Roff
0.1%
Shell
0.1%
Emacs Lisp
0.1%

Contributors