kayuri/HNC — Issue #26: Develop a semantic of HN0 in Ott
Author: nponeccop
Created: 2011-10-16 07:20:47+00:00
State: open

http://www.cl.cam.ac.uk/~pes20/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.