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 22 articles , 2 standard articles )

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

1 2 next

  1. Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
  2. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  3. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  4. Breitner, Joachim; Eisenberg, Richard A.; Peyton Jones, Simon; Weirich, Stephanie: Safe zero-cost coercions for Haskell (2016)
  5. Eades, Harley III; Stump, Aaron; McCleeary, Ryan: Dualized simple type theory (2016)
  6. Stansifer, Paul; Wand, Mitchell: Romeo: a system for more flexible binding-safe programming (2016)
  7. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  8. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  9. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)
  10. Sewell, Peter: Tales from the jungle (2012) ioport
  11. Krebbers, Robbert; Wiedijk, Freek: A formalization of the C99 standard in HOL, Isabelle and Coq (2011)
  12. Owens, Scott; Böhm, Peter; Zappa Nardelli, Francesco; Sewell, Peter: Lem: a lightweight tool for heavyweight semantics (2011)
  13. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2011)
  14. Weirich, Stephanie; Yorgey, Brent A.; Sheard, Tim: Binders unbound (2011)
  15. 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)
  16. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)
  17. Ellison, Chucky; Şerbănuţă, Traian Florin; Roşu, Grigore: A rewriting logic approach to type inference (2009)
  18. Schäfer, Max; Ekman, Torbjörn; de Moor, Oege: Formalising and verifying reference attribute grammars in Coq (2009)
  19. Kaufmann, Matt; Moore, J. Strother: An ACL2 tutorial (2008)
  20. Slind, Konrad; Norrish, Michael: A brief overview of HOL4 (2008)

1 2 next