search

nponeccop / HNC

HN Compiler
GNU Lesser General Public License v3.0
62 stars 5 forks source link

Develop a semantic of HN0 in Ott #26

Open nponeccop opened 12 years ago

nponeccop commented 12 years ago

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.