Ott swMATH ID: 663 Software Authors: Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok Description: 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. Homepage: http://www.cl.cam.ac.uk/~pes20/ott/ Related Software: Coq; Isabelle/HOL; Nominal Isabelle; Isabelle; Twelf; PoplMark; HOL; OCaml; ML; K Prover; Abella; HYBRID; Freshml; Haskell; ACL2; Spoofax; ELPI; Beluga; Maude; JavaScript Cited in: 33 Documents Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Ott: effective tool support for the working semanticist. Zbl 1185.68201Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok 2010 Ott, effective tool support for the working semanticist. Zbl 1291.68238Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok 2007 all top 5 Cited by 72 Authors 3 Owens, Scott 3 Ridge, Thomas 3 Roşu, Grigore 3 Sewell, Peter 3 Zappa Nardelli, Francesco 2 Bhargavan, Karthikeyan 2 Chen, Juan 2 Cimini, Matteo 2 Fournet, Cédric 2 Momigliano, Alberto 2 Peskine, Gilles 2 Sarkar, Susmit 2 Strniša, Rok 2 Strub, Pierre-Yves 2 Swamy, Nikhil 2 Weirich, Stephanie 2 Yang, Jean 1 Azevedo de Amorim, Arthur 1 Bettini, Lorenzo 1 Blazy, Sandrine 1 Bodin, Martin 1 Böhm, Peter 1 Breitner, Joachim 1 Charguéraud, Arthur 1 Cheney, James 1 de Moor, Oege 1 Eades, Harley III 1 Eisenberg, Richard A. 1 Ekman, Torbjörn 1 Ellison, Chucky 1 Farka, František 1 Felty, Amy P. 1 Filaretti, Daniele 1 Gardner, Philippa Anne 1 Gheri, Lorenzo 1 Johansen, Christian 1 Kaliszyk, Cezary 1 Kamareddine, Fairouz D. 1 Kaufmann, Matt 1 Krebbers, Robbert 1 Lakin, Matthew R. 1 Leroy, Xavier 1 Maffeis, Sergio 1 Mccleeary, Ryan 1 Miller, Dale Allen 1 Moore, Brandon M. 1 Moore, J Strother 1 Mosses, Peter D. 1 Mourad, Benjamin 1 Naudziuniene, Daiva 1 Norrish, Michael 1 Owe, Olaf 1 Peña, Lucas 1 Peyton Jones, Simon L. 1 Pitts, Andrew M. 1 Popescu, Andrei 1 Quinlan, Dee 1 Schäfer, Max 1 Schmitt, Alan 1 Sculthorpe, Neil 1 Şerbănuţă, Traian Florin 1 Sheard, Tim 1 Slind, Konrad 1 Smith, Gareth David 1 Stansifer, Paul 1 Stump, Aaron 1 Urban, Christian 1 van Binsbergen, L. Thomas 1 Wand, Mitchell 1 Wells, Joe B. 1 Wiedijk, Freek 1 Yorgey, Brent A. all top 5 Cited in 6 Serials 5 Journal of Automated Reasoning 4 Journal of Functional Programming 3 Journal of Logical and Algebraic Methods in Programming 1 Theoretical Computer Science 1 Theory and Practice of Logic Programming 1 Logical Methods in Computer Science Cited in 3 Fields 32 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 1 Category theory; homological algebra (18-XX) Citations by Year