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
Sep 11, 2024 10:37am 0 VERSION_BUMP 16177906
Dec 1, 2023 7:00pm 0 VERSION_BUMP d1b8da91
« Back to VersTracker  |  Browse Packages  |  About