{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T23:17:02Z","timestamp":1776122222965,"version":"3.50.1"},"reference-count":76,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2010,1,26]],"date-time":"2010-01-26T00:00:00Z","timestamp":1264464000000},"content-version":"unspecified","delay-in-days":25,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2010,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available <jats:italic>metalanguages<\/jats:italic> for expressing semantics \u2013 usually either <jats:private-char><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0956796809990293_char1\"\/><\/jats:private-char> for informal mathematics or the formal mathematics of a proof assistant \u2013 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 <jats:private-char><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0956796809990293_char1\"\/><\/jats:private-char> 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 (OCaml<jats:sub><jats:italic>light<\/jats:italic><\/jats:sub>, 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.<\/jats:p>","DOI":"10.1017\/s0956796809990293","type":"journal-article","created":{"date-parts":[[2010,1,26]],"date-time":"2010-01-26T14:01:27Z","timestamp":1264514487000},"page":"71-122","source":"Crossref","is-referenced-by-count":102,"title":["Ott: Effective tool support for the working semanticist"],"prefix":"10.1017","volume":"20","author":[{"given":"PETER","family":"SEWELL","sequence":"first","affiliation":[]},{"given":"FRANCESCO ZAPPA","family":"NARDELLI","sequence":"additional","affiliation":[]},{"given":"SCOTT","family":"OWENS","sequence":"additional","affiliation":[]},{"given":"GILLES","family":"PESKINE","sequence":"additional","affiliation":[]},{"given":"THOMAS","family":"RIDGE","sequence":"additional","affiliation":[]},{"given":"SUSMIT","family":"SARKAR","sequence":"additional","affiliation":[]},{"given":"ROK","family":"STRNI\u0160A","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2010,1,26]]},"reference":[{"key":"S0956796809990293_ref39","first-page":"73","volume-title":"Compiler Construction, 13th International Conference, CC 2004, Proceedings","author":"McPeak","year":"2004"},{"key":"S0956796809990293_ref73","unstructured":"Xiao Y. , Ariola Z & Mauny M. (2000) From syntactic theories to interpreters: A specification language and its compilation. In First International Workshop on Rule-Based Programming (RULE 2000), Derschowitz N. & Kirchner C. (eds). Available at: http:\/\/arxiv.org\/abs\/cs.PL\/0009030 Accessed 8 January 2010."},{"key":"S0956796809990293_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"S0956796809990293_ref63","unstructured":"Strachey C. (1966) Towards a formal semantics. In Formal Language Description Languages for Computer Programming. North Holland, pp. 198\u2013220."},{"key":"S0956796809990293_ref4","doi-asserted-by":"crossref","unstructured":"Aydemir B. , Chargu\u00e9raud A. , Pierce B. C. , Pollack R. & Weirich S. (2008) Engineering Formal Metatheory. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '08). ACM, San Francisco, pp. 3\u201315.","DOI":"10.1145\/1328438.1328443"},{"key":"S0956796809990293_ref49","volume-title":"Haskell 98 Language and Libraries. The Revised Report","author":"Peyton Jones","year":"2003"},{"key":"S0956796809990293_ref75","volume-title":"A Semantic Definition of Separate Type Checking in C++ with Concepts\u2014Abstract Syntax and Complete Semantic Definition","author":"Zalewski","year":"2008"},{"key":"S0956796809990293_ref42","unstructured":"Moors A. , Piessens F. & Odersky M. (2008) Safe type-level abstraction in Scala. International Workshop on Foundations of Object-Oriented Languages. FOOL workshop, San Francisco. http:\/\/fool08.kuis.kyoto-u.ac.jp\/program.html Accessed 8 January 2010."},{"key":"S0956796809990293_ref18","doi-asserted-by":"crossref","unstructured":"Delaware B. , Cook W. & Batory D. (2009) A machine-checked model of safe composition. In Proceedings of the 8th Workshop on Foundations of Aspect-Oriented Languages (FOAL), Charlottesville, Virginia, ACM pp. 31\u201335.","DOI":"10.1145\/1509837.1509846"},{"key":"S0956796809990293_ref54","unstructured":"Rekers J. (1992) Parser Generation for Interactive Environments. Ph.D. Thesis, University of Amsterdam."},{"key":"S0956796809990293_ref16","unstructured":"Coq. (2008). The Coq proof assistant, v.8.1. Available at: http:\/\/coq.inria.fr\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref61","doi-asserted-by":"crossref","unstructured":"Shinwell M. R. , Pitts A. M. & Gabbay M. J. (2003) FreshML: Programming with binders made simple. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003). ACM, Uppsala, pp. 263\u2013274.","DOI":"10.1145\/944746.944729"},{"key":"S0956796809990293_ref28","volume-title":"Mistakes and Ambiguities in the Definition of Standard ML","author":"Kahrs","year":"1993"},{"key":"S0956796809990293_ref52","unstructured":"Pollack R. (2006) Reasoning about languages with binding. Available at: http:\/\/homepages.inf.ed.ac.uk\/rpollack\/export\/bindingChallenge_slides.pdf. Slides. Accessed 8 January 2010."},{"key":"S0956796809990293_ref19","first-page":"30","volume-title":"Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Proceedings","author":"Dijkstra","year":"2006"},{"key":"S0956796809990293_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/151257.151260"},{"key":"S0956796809990293_ref55","doi-asserted-by":"crossref","unstructured":"Reps T. & Teitelbaum T. (1984) The synthesizer generator. In Proceedings of the first ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (SDE 1), Pittsburgh, pp. 42\u201348. http:\/\/portal.acm.org\/citation.cfm?id=390010.808247 Accessed 8 January 2010.","DOI":"10.1145\/800020.808247"},{"key":"S0956796809990293_ref27","volume-title":"Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"Jia","year":"2009"},{"key":"S0956796809990293_ref23","volume-title":"Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"Greenberg","year":"2009"},{"key":"S0956796809990293_ref50","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796809990293_ref15","first-page":"269","volume-title":"Logic Programming, 20th International Conference, ICLP 2004, Proceedings","author":"Cheney","year":"2004"},{"key":"S0956796809990293_ref6","first-page":"2","volume-title":"Smart Card Programming and Security, International Conference on Research in Smart Cards, E-smart 2001, Proceedings","author":"Barthe","year":"2001"},{"key":"S0956796809990293_ref76","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.5.a2"},{"key":"S0956796809990293_ref47","doi-asserted-by":"crossref","unstructured":"Owens S. & Flatt M. (2006) From structures and functors to modules and units. In Proceedings of 11th ACM SIGPLAN International Conference on Functional Programming (ICFP 2006). ACM, Portland, Oregon, pp. 87\u201398.","DOI":"10.1145\/1160074.1159815"},{"key":"S0956796809990293_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001933"},{"key":"S0956796809990293_ref62","unstructured":"Sperber M. , Dybvig R. K. , Flatt M. , Anton Van Straaten K. , Richard C. , William J. R. (eds), Revised5 Report on the Algorithmic Language Scheme, Findler, R. B. & Jacob M. (Authors, formal semantics). (2007) Revised6 report on the algorithmic language Scheme. Available at: http:\/\/www.r6rs.org\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref11","doi-asserted-by":"crossref","unstructured":"Borras P. , Cl\u00e9ment D. , Despeyroux T. , Incerpi J. , Kahn G. , Lang B. & Pascual V. (1988) CENTAUR: The system. In Proceedings of the third ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (SDE 3). ACM, pp. 14\u201324.","DOI":"10.1145\/64135.65005"},{"key":"S0956796809990293_ref12","first-page":"81","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Third International Workshop, TACAS '97, Proceedings","author":"Boulton","year":"1997"},{"key":"S0956796809990293_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"S0956796809990293_ref40","doi-asserted-by":"crossref","unstructured":"Milner R. (1972) Implementation and applications of Scott's logic for computable functions. In Proceedings ACM Conference on Proving Assertions About Programs, ACM, Las Cruces, New Mexico, pp. 1\u20136.","DOI":"10.1145\/800235.807067"},{"key":"S0956796809990293_ref14","unstructured":"Chargu\u00e9raud A. (2006) Annotated bibliography for formalization of lambda-calculus and type theory. Available at: http:\/\/arthur.chargueraud.org\/projects\/binders\/biblio.php Accessed 8 January 2010."},{"key":"S0956796809990293_ref72","unstructured":"Visser E. (1997) Syntax Definition for Language Prototyping. Ph.D. Thesis, University of Amsterdam."},{"key":"S0956796809990293_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"S0956796809990293_ref13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"S0956796809990293_ref2","first-page":"38","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Proceedings","author":"Aspinall","year":"2000"},{"key":"S0956796809990293_ref71","unstructured":"VanInwegen M. (1996) The Machine-Assisted Proof of Programming Language Properties. Ph.D. Thesis, University of Pennsylvania. Computer and Information Science Tech Report MS-CIS-96-31."},{"key":"S0956796809990293_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_4"},{"key":"S0956796809990293_ref58","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006442"},{"key":"S0956796809990293_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"S0956796809990293_ref56","unstructured":"Rossberg A. (2001) Defects in the Revised Definition of Standard ML. Tech. Rep., Saarland University. Updated 2007\/01\/22."},{"key":"S0956796809990293_ref7","unstructured":"Benton N. & Koutavas V. (2007) A mechanized bisimulation for the nu-calculus. Available at: http:\/\/research.microsoft.com\/en-us\/um\/people\/nick\/nubisim.pdf Accessed 8 January 2010."},{"key":"S0956796809990293_ref45","unstructured":"Owens C. (1995) Coding binding and substitution explicitly in Isabelle. In Proceedings of the First Isabelle Users Workshop, Cambridge, pp. 36\u201352. Available at: http:\/\/www.cl.cam.ac.uk\/lp15\/papers\/Workshop\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref60","doi-asserted-by":"crossref","unstructured":"Sewell P. , Zappa Nardelli F. , Owens S. , Peskine G. , Ridge T. , Sarkar S. & Strni\u0161a R. (2007b) Ott: Effective tool support for the working semanticist. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007). ACM, pp. 1\u201312.","DOI":"10.1145\/1291220.1291155"},{"key":"S0956796809990293_ref32","first-page":"19","volume-title":"Eighth Symposium on Trends in Functional Programming (TFP 2007)","author":"Lakin","year":"2007"},{"key":"S0956796809990293_ref51","first-page":"122","volume-title":"Mathematical Foundations of Computer Science, 18th International Symposium, MFCS'93, Proceedings","author":"Pitts","year":"1993"},{"key":"S0956796809990293_ref25","unstructured":"HOL. (2007) The HOL 4 system, Kananaskis-4 release. Available at: http:\/\/hol.sourceforge.net\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref65","first-page":"43","volume-title":"Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Proceedings","author":"Syme","year":"1993"},{"key":"S0956796809990293_ref33","doi-asserted-by":"crossref","unstructured":"Lee D. K. , Crary K. & Harper R. (2007) Towards a Mechanized Metatheory of Standard ML. In Proceedings 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, Nice, pp. 173\u2013184.","DOI":"10.1145\/1190216.1190245"},{"key":"S0956796809990293_ref74","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014408032446"},{"key":"S0956796809990293_ref66","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60043-4_56"},{"key":"S0956796809990293_ref68","unstructured":"Twelf. (2005). Twelf 1.5. Available at: http:\/\/www.cs.cmu.edu\/twelf\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref57","volume-title":"Acute: High-Level Programming Language Design for Distributed Computation. Design Rationale and Language Definition","author":"Sewell","year":"2004"},{"key":"S0956796809990293_ref26","unstructured":"Isabelle. (2008) Isabelle 2008. Available at: http:\/\/isabelle.in.tum.de\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref3","first-page":"50","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Proceedings","author":"Aydemir","year":"2005"},{"key":"S0956796809990293_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"S0956796809990293_ref53","doi-asserted-by":"crossref","unstructured":"Pottier F. (2006) An overview of C\u03b1ml. In ACM Workshop on ML, ENTCS, vol. 148, no. 2, pp. 27\u201352.","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"S0956796809990293_ref41","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796809990293_ref5","unstructured":"Aydemir B. & Weirich S. (2009) LNgen: Tool support for locally nameless representation. Available at: http:\/\/www.cis.upenn.edu\/baydemir\/papers\/lngen\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref38","first-page":"301","volume-title":"Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Proceedings","author":"Matthews","year":"2004"},{"key":"S0956796809990293_ref8","doi-asserted-by":"crossref","unstructured":"Berghofer S. & Urban C. (2006) A head-to-head comparison of de Bruijn indices and names. In Proceedings of International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), ENTCS 174(5), pp. 53\u201367.","DOI":"10.1016\/j.entcs.2007.01.018"},{"key":"S0956796809990293_ref67","volume-title":"Concise Concrete Syntax","author":"Tse","year":"2008"},{"key":"S0956796809990293_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_72"},{"key":"S0956796809990293_ref64","doi-asserted-by":"crossref","unstructured":"Strni\u0161a R. , Sewell P. & Parkinson M. (2007) The Java module system: Core design and semantic definition. In Proceedings of ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2007). ACM, Montreal, pp. 499\u2013514.","DOI":"10.1145\/1297105.1297064"},{"key":"S0956796809990293_ref59","unstructured":"Sewell P. & Zappa Nardelli F. (2007) Ott, Freiburg. Available at: http:\/\/www.cl.cam.ac.uk\/users\/pes20\/ott\/ Accessed 8 January 2010."},{"key":"S0956796809990293_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61604-7_67"},{"key":"S0956796809990293_ref21","first-page":"383","volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Proceedings","author":"Fournet","year":"2008"},{"key":"S0956796809990293_ref35","unstructured":"Leroy X. , Doligez D. , Garrigue J. , R\u00e9my D. & Vouillon J. (2005) The Objective Caml System Release 3.09 Documentation and User's Manual. URL http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/(3.11 from 2008) Accessed 8 January 2010."},{"key":"S0956796809990293_ref43","doi-asserted-by":"crossref","unstructured":"Mosses P. D. (2002) Pragmatics of modular SOS. In Proceedings of 9th International Conference on Algebraic Methodology and Software Technology (AMAST '02), LNCS 2442, Kirchner H. & Ringeissen C. (eds), Lecture Notes in Computer Science, vol. 2422. Springer, Saint-Gilles-les-Bains, pp. 21\u201340.","DOI":"10.1007\/3-540-45719-4_3"},{"key":"S0956796809990293_ref24","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.2.142"},{"key":"S0956796809990293_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004550"},{"key":"S0956796809990293_ref44","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-49099-X_10","volume-title":"Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, Proceedings","author":"Norrish","year":"1999"},{"key":"S0956796809990293_ref34","doi-asserted-by":"crossref","unstructured":"Lee P. , Pfenning F. , Rollins G. & Scherlis W. (1988) The Ergo Support System: An integrated set of tools for prototyping integrated environments. In Proceedings of ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, ACM, Boston, pp. 25\u201334.","DOI":"10.1145\/64137.65006"},{"key":"S0956796809990293_ref1","doi-asserted-by":"crossref","unstructured":"Aldrich J. , Simmons R. J. & Shin K. (2008) SASyLF: An Educational Proof Assistant for Language Theory. In Proceedings of the 2008 International Workshop on Functional and Declarative Programming in Education (FDPE '08). ACM, Victoria, BC, pp. 31\u201340.","DOI":"10.1145\/1411260.1411266"},{"key":"S0956796809990293_ref30","unstructured":"Klein G. , Nipkow T. & Paulson L. (eds) (2009) The archive of formal proofs. Available at: http:\/\/afp.sf.net Accessed 8 January 2010."},{"key":"S0956796809990293_ref46","first-page":"1","volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Proceedings","author":"Owens","year":"2008"},{"key":"S0956796809990293_ref48","unstructured":"Peskine G. , Sarkar S. , Sewell P. & Zappa Nardelli F. (2007) Binding and substitution (note). Available at: http:\/\/www.cl.cam.ac.uk\/users\/pes20\/ott\/ Accessed 8 January 2010."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796809990293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T21:01:32Z","timestamp":1556485292000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796809990293\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":76,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["S0956796809990293"],"URL":"https:\/\/doi.org\/10.1017\/s0956796809990293","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1]]}}}