topic.ott.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"ott" -ob topic.ott.bib sewellbib2.bib}}

@inproceedings{ott-sub,
  author = {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
  title = {{Ott}: Effective Tool Support for the Working Semanticist},
  optcrossref = {},
  optkey = {},
  conf = {ICFP 2007},
  booktitle = {Proceedings of {the 12th ACM SIGPLAN International Conference on Functional Programming (Freiburg)}},
  pages = {1--12},
  numpages = {12},
  opturl = {http://doi.acm.org/10.1145/1291151.1291155},
  doi = {10.1145/1291151.1291155},
  year = {2007},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = oct,
  optorganization = {},
  optpublisher = {},
  note = {ACM SIGPLAN Most Influential ICFP Paper Award 2017 (for 2007)},
  optannote = {},
  project = {http://www.cl.cam.ac.uk/~pes20/ott/},
  pdf = {http://www.cl.cam.ac.uk/~pes20/ott/paper.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/ott/paper.ps},
  abstract = {It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTeX 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, Isabelle, and (in progress) Twelf, 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 (around 306 rules), with machine 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.},
  topic = {ott}
}

@article{ott-jfp,
  author = {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
  title = {{Ott}: Effective Tool Support for the Working Semanticist},
  optcrossref = {},
  optkey = {},
  optjournal = {J. Functional Programming},
  journal = {Journal of Functional Programming},
  year = {2010},
  optkey = {},
  volume = {20},
  number = {1},
  pages = {70--122},
  month = jan,
  note = {Invited submission from ICFP 2007, which was awarded the ACM SIGPLAN Most Influential ICFP 2007 Paper, in 2017},
  optannote = {},
  project = {http://www.cl.cam.ac.uk/~pes20/ott/},
  doi = {https://doi.org/10.1017/S0956796809990293},
  pdf = {http://www.cl.cam.ac.uk/~pes20/ott/ott-jfp.pdf},
  abstract = {
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 LaTeX 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 (OCamllight, 310 rules), 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.},
  topic = {ott}
}

@inproceedings{WMM10,
  author = {Stephanie Weirich and Scott Owens and Peter Sewell and Zappa Nardelli, Francesco},
  title = {{Ott} or {Nott}},
  month = sep,
  year = 2010,
  note = {2pp},
  conf = {WMM 2010},
  booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Mechanizing Metatheory},
  project = {http://www.cl.cam.ac.uk/~pes20/ott/},
  pdf = {https://www.cl.cam.ac.uk/~pes20/ott/wmm2010.pdf},
  abstract = {
Ott: This talk discusses the experience of using Ott for programming 
language design. Or Nott? 
We reflect on the limitations of Ott, and on what other (New Ott?)
 tool support a working semanticist might want in an ideal world.
},
  topic = {ott}
}

@misc{ott-release,
  optkey = {},
  author = {Peter Sewell and Zappa Nardelli, Francesco},
  title = {Ott release, version 0.10.9},
  opthowpublished = {},
  month = aug,
  year = {2007},
  note = {\url{http://www.cl.cam.ac.uk/~pes20/ott/}},
  url = {http://www.cl.cam.ac.uk/~pes20/ott/},
  project = {http://www.cl.cam.ac.uk/~pes20/ott/},
  optannote = {},
  topic = {ott}
}