Ott

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

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

1 2 next

  1. Johansen, Christian; Owe, Olaf: Dynamic structural operational semantics (2019)
  2. Miller, Dale: Mechanized metatheory Revisited (2019)
  3. van Binsbergen, L. Thomas; Mosses, Peter D.; Sculthorpe, Neil: Executable component-based semantics (2019)
  4. Moore, Brandon; Peña, Lucas; Rosu, Grigore: Program verification by coinduction (2018)
  5. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  6. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  7. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  8. Breitner, Joachim; Eisenberg, Richard A.; Peyton Jones, Simon; Weirich, Stephanie: Safe zero-cost coercions for Haskell (2016)
  9. Eades, Harley III; Stump, Aaron; McCleeary, Ryan: Dualized simple type theory (2016)
  10. Stansifer, Paul; Wand, Mitchell: Romeo: a system for more flexible binding-safe programming (2016)
  11. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  12. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
  13. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  14. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)
  15. Sewell, Peter: Tales from the jungle (2012) ioport
  16. Krebbers, Robbert; Wiedijk, Freek: A formalization of the C99 standard in HOL, Isabelle and Coq (2011)
  17. Owens, Scott; Böhm, Peter; Zappa Nardelli, Francesco; Sewell, Peter: Lem: a lightweight tool for heavyweight semantics (2011)
  18. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2011)
  19. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2011)
  20. Weirich, Stephanie; Yorgey, Brent A.; Sheard, Tim: Binders unbound (2011)

1 2 next