Ott: Effective Tool Support for the Working Semanticist

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

*Corresponding author for this work

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

37 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationICFP'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING
Place of PublicationNEW YORK
PublisherACM
Pages1-12
Number of pages12
ISBN (Print)978-1-59593-815-2
DOIs
Publication statusPublished - 2007
Event12th ACM SIGPLAN International Conference on Functional Programming - Freiburg, Germany
Duration: 1 Oct 20073 Oct 2007

Conference

Conference12th ACM SIGPLAN International Conference on Functional Programming
Country/TerritoryGermany
CityFreiburg
Period1/10/073/10/07

Keywords

  • Standardization
  • Verification
  • Theory
  • Languages

Fingerprint

Dive into the research topics of 'Ott: Effective Tool Support for the Working Semanticist'. Together they form a unique fingerprint.

Cite this