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}
}