TY - JOUR
T1 - Ott
T2 - Effective tool support for the working semanticist
AU - Sewell, Peter
AU - Nardelli, Francesco Zappa
AU - Owens, Scott
AU - Peskine, Gilles
AU - Ridge, Thomas
AU - Sarkar, Susmit
AU - Strnisa, Rok
PY - 2010/1
Y1 - 2010/1
N2 - Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics usually either L(A)T(E)X 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, and Isabelle/HOL, together with L(A)T(E)X 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 ill Substantial ease Studies, including modular Specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCaml(light), 310 rules). with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, With rigorous semantic definitions of realistic languages.
AB - Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics usually either L(A)T(E)X 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, and Isabelle/HOL, together with L(A)T(E)X 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 ill Substantial ease Studies, including modular Specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCaml(light), 310 rules). with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, With rigorous semantic definitions of realistic languages.
KW - SYSTEMS
KW - COMPILER
KW - LOGIC
KW - PROGRAMMING LANGUAGE
U2 - 10.1017/S0956796809990293
DO - 10.1017/S0956796809990293
M3 - Article
SN - 0956-7968
VL - 20
SP - 71
EP - 122
JO - Journal of Functional Programming
JF - Journal of Functional Programming
IS - 01
ER -