Skip to content

Research at St Andrews

Ott: Effective tool support for the working semanticist

Research output: Contribution to journalArticle

DOI

Author(s)

Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa

School/Research organisations

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 U 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.

Close

Details

Original languageEnglish
Pages (from-to)1-12
Number of pages12
JournalACM SIGPLAN Notices
Volume42
Issue number9
DOIs
StatePublished - Sep 2007
Event12th ACM SIGPLAN International Conference on Functional Programming - Freiburg, Germany
Duration: 1 Oct 20073 Oct 2007

    Research areas

  • languages, verification, theory, standardization

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S. 27 Aug 2018 The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  3. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P. Jan 2018 Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, Vol. 2 Issue POPL, 29 p. 19

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Verification of a lazy cache coherence protocol against a weak memory model

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V. 2 Oct 2017 Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD). ACM, p. 60-67

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P. 1 Jan 2017 Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages. ACM, p. 429-442

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related by journal

  1. Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER

    Batty, M., Memarian, K., Owens, S., Sarkar, S. & Sewell, P. Jan 2012 In : ACM SIGPLAN Notices. 47, 1, p. 509-520 12 p.

    Research output: Contribution to journalArticle

  2. Synchronising C/C plus plus and POWER

    Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. & Williams, D. Jun 2012 In : ACM SIGPLAN Notices. 47, 6, p. 311-321 11 p.

    Research output: Contribution to journalArticle

  3. Mathematizing C++ Concurrency

    Batty, M., Owens, S., Sarkar, S., Sewell, P. & Weber, T. Jan 2011 In : ACM SIGPLAN Notices. 46, 1, p. 55-66 12 p.

    Research output: Contribution to journalArticle

  4. Understanding POWER Multiprocessors

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L. & Williams, D. Jun 2011 In : ACM SIGPLAN Notices. 46, 6, p. 175-186 12 p.

    Research output: Contribution to journalArticle

  5. The Semantics of x86-CC Multiprocessor Machine Code

    Sarkar, S., Sewell, P., Nardelli, F. Z., Owens, S., Ridge, T., Braibant, T., Myreen, M. O. & Alglave, J. Jan 2009 In : ACM SIGPLAN Notices. 44, 1, p. 379-391 13 p.

    Research output: Contribution to journalArticle

ID: 44377042