Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

The Caml Hump: Ott


tool for semantic definitions of programming languages and calculi. The tool takes as input a definition of a language syntax and semantic relations, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It builds parsers for symbolic and concrete terms of the language, generates LaTeX to build a typeset version of the definition, and generates Coq, HOL, and Isabelle versions of the definition.
Homepage ]
Author:Francesco Zappa Nardelli and Peter Sewell.
Last modification date:08-Jan-2007
Development status:Alpha
Kind: Applications written in Caml
License: Open Source :: BSD
Topic: Science :: Computing
Science :: Maths and Logic