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 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 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, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml, 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.

References in zbMATH (referenced in 16 articles , 2 standard articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  2. Eades, Harley III; Stump, Aaron; McCleeary, Ryan: Dualized simple type theory (2016)
  3. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  4. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  5. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)
  6. Sewell, Peter: Tales from the jungle (2012) ioport
  7. Owens, Scott; Böhm, Peter; Zappa Nardelli, Francesco; Sewell, Peter: Lem: a lightweight tool for heavyweight semantics (2011)
  8. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2011)
  9. Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok: Ott: effective tool support for the working semanticist (2010)
  10. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)
  11. Ellison, Chucky; Şerbănuţă, Traian Florin; Roşu, Grigore: A rewriting logic approach to type inference (2009)
  12. Schäfer, Max; Ekman, Torbjörn; de Moor, Oege: Formalising and verifying reference attribute grammars in Coq (2009)
  13. Kaufmann, Matt; Moore, J. Strother: An ACL2 tutorial (2008)
  14. Slind, Konrad; Norrish, Michael: A brief overview of HOL4 (2008)
  15. Ridge, Tom: Operational reasoning for concurrent Caml programs and weak memory models (2007)
  16. Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok: Ott, effective tool support for the working semanticist (2007)