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

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

1 2 next

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

1 2 next