Sciweavers

Share
ICFP
2007
ACM

Ott: effective tool support for the working semanticist

10 years 7 months ago
Ott: effective tool support for the working semanticist
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics -- usually either LATEX for informal mathematics, or the formal mathematics of a proof assistant -- make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, Isabelle, and (in progress) Twelf, together with LATEX code for production-quality typesetting, and OCaml boilerplate. The main innovations are: (1) metalanguage design to make definitions concise, and easy to read and edit; (2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code. This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text,...
Peter Sewell, Francesco Zappa Nardelli, Scott Owen
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2007
Where ICFP
Authors Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa
Comments (0)
books