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 |