Ott is a tool for writing definitions of programming languages and calculi. 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, Isabelle, and Lem versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL/Lem source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by targetsystem terms. For a simple example, here is an Ott source file for an untyped callbyvalue lambda calculus, and the generated LaTeX (compiled to pdf), Coq, Isabelle, HOL, and Lem definitions.
Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates goodquality typeset output. By parsing (and so sortchecking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.
That same input can be used to generate formal definitions, for Coq, HOL, Isabelle, and Lem. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. At present only a fully concrete representation of binding, without quotienting by alpha equivalence, is fully supported. An experimental backend generates a locallynameless representation of terms for a subset of the Ott metalanguage: details can be found here.
The initial work on Ott developed several examples: untyped and simply typed lambdacalculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment. Ott was also initially used for more substantial work on iJAM and LJAM, Java Module Systems, by Rok Strniša, and semantics for OCaml light, by Scott Owens. Since then, it has been used in a number of projects, by us and by others.
We would like to collect bibtex data for any papers written using Ott. Please send these to Peter Sewell or Francesco Zappa Nardelli.
The following are examples from the original development. They have not necessarily been updated to the current version of Ott or of each of the theoremprover backends. See the github repository for the most recent available versions.
System  Rules  Ott sources  Latex  Typeset  Dot  Coq  HOL  Isabelle  

Defn  Proof  Defn  Proof  Defn  Proof  
Untyped CBV lambda  3  test10.ott 
test10.tex 
(ps)  test10.v 
test10Script.sml 
test10.thy 

Simply typed CBV lambda  6  test10st.ott 
test10st.tex 
(ps)  test10st.v 
test10st_metatheory.v 
test10stScript.sml 
test10st_metatheoryScript.sml 
test10st.thy 
test10st_metatheory.thy 

ML polymorphism  22  test8.ott 
test8.tex 
(ps)  test8.v 
test8Script.sml 
test8.thy 

TAPL roughlyfullsimple  63  (sources)  (ps)  (Coq (including records))  (HOL)  (script)  (Isabelle)  (script)  
POPLmark Fsub (*)  48  (sources)  (latex)  (pdf) (ps)  
Leroy JFP96 module system (*)  67  leroyjfp96.ott 
(latex)  (ps)  (HOL)  
LJ: Lightweight Java  85  (sources)  (pdf)  (Isabelle)  (zip)  
LJAM: Java Module System  163  (sources)  (pdf)  (Isabelle)  (zip)  
OCaml light  310  (sources)  (ps)  (ps)  (Coq)  (HOL)  (scripts)  (Isabelle) 
(all files except the proof scripts are generated from the Ott sources)
(*) These systems would need explicit alpha conversion in the rules to capture the intended semantics using the fully concrete representation.