Version française
Home     About     Download     Resources     Contact us    

The Caml Hump: Ott

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
Version:0.10.2
Development status:Alpha
Kind: Applications written in Caml
License: Open Source :: BSD
Topic: Science :: Computing
Science :: Maths and Logic
Homepage:http://moscova.inria.fr/~zappa/software/ott