LogoopenSUSE Build Service > Projects
Sign Up | Log In


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.

Source Files

Filename Size Changed Actions
ott.spec 4.54 KB Download File
ott_distro_0.10.14.tar.gz 2.56 MB Download File

Comments for home:marcinzalewski (0)

Login required, please login or signup in order to comment