[POPLmark Fsub dependency diagram]

Ott

Francesco Zappa Nardelli, Peter Sewell, and Scott Owens

(with Matthew Parkinson, Gilles Peskine, Tom Ridge, Susmit Sarkar, and Rok Strniša)

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, 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. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL 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 good-quality typeset output. By parsing (and so sort-checking) 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 (experimentally) 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 locally-nameless representation of terms for a subset of the Ott metalanguage: details can be found here.

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, 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. More substantially, Ott has been used for work on iJAM and LJAM, Java Module Systems, by Rok Strniša, and semantics for OCaml light, by Scott Owens.

A release of the Ott source is available, and comment and feedback would be much appreciated.

Papers and Documentation

Code

Bug Tracker

Mailing Lists

Examples

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 roughly-full-simple 63 (sources) (ps) (Coq (including records)) (HOL) (script) (Isabelle) (script)
POPLmark Fsub (*) 48 (sources) (latex) (pdf)   (ps)
Leroy JFP96 module system (*) 67 leroy-jfp96.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.


[validate]