ott ☆

« Back to VersTracker

Description:
Tool for writing definitions of programming languages and calculi

Type: Formula | Tracked Since: Dec 28, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: formal-methods programming-languages semantics latex coq

Install: brew install ott

About:
Ott is a tool designed for writing definitions of programming languages and calculi. It generates LaTeX and HTML documentation from a concise source format, ensuring consistency between the specification and its presentation. It also produces Coq code for mechanized proofs, bridging the gap between informal and formal semantics.

Key Features:

Generates LaTeX and HTML from a single source
Produces Coq code for formal verification
Defines syntax, typing rules, and operational semantics
Checks for rule consistency and variable binding

Use Cases:

Drafting formal semantics for a new programming language
Creating consistent documentation for language specifications
Generating Coq definitions for mechanizing type safety proofs

Alternatives:

BNFC – BNFC focuses on generating parsers and abstract syntax trees, whereas Ott specializes in typesetting and formalizing semantics.
Lem – Lem is a tool for generating definitions and proofs for multiple proof assistants, similar to Ott's Coq backend but with a different language focus.

Version History

Detected	Version	Rev	Change	Commit
Sep 16, 2025 10:13am		0	VERSION_BUMP	a16f9fb4
Dec 30, 2024 11:09am		0	VERSION_BUMP	096141ae