«
»

Ott

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.

This entry was posted on Sunday, December 23rd, 2007 at 12:33 pm and is filed under Semantic assistants. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

One Response to “Ott”

  1. dontsnipe Says:
    September 2nd, 2010 at 7:59 am

    To all you industrial, construction, and hard laborers, CAT was created. CAT boots are known to be some of the most durable and sturdy boots there are on the market. Just holler if you are interested in CAT boots.

Leave a Reply