- By James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough.
- Presented at ICFP 2003.
- Download in postscript or pdf. Or get US-letter-sized postscript.
-
- §4.3.4 Expression reduction,
rule
ered.col.tuple -
The values are hm' values, not hm values.
The corrected rule reads:
_{hm} ([v_1^{hm'}]_{hm'}^{T_1},...,[v_j^{hm'}]_{hm'}^{T_j})">
- §4.3.4 Expression reduction,
rule
ered.col.fun -
The coloured brackets around the variable in the right-hand
side were wrong.
The rule corrected rule reads:
T''} -->_{hm} \x:T'. [\{x<-[x]_{hm'}^{T}\}e]_{hm'}^{T''}">
In the technical report, the proof of the corresponding case of Theorem G.15 (type preservation for expression reduction) has also been corrected accordingly.
- §4.3.4 Expression reduction,
rule
-
A longer version of this paper appeared as INRIA technical report RR-4851.
- By James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough.
- INRIA technical report RR-4851.
- Nicknamed the ``Hashed-abstract-types'' document.
- Download the bug-fixed version in postscript or pdf. (The original, official INRIA research report is also available here).
- This report is a superset of the companion ICFP article.
-
Abstract:
Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this report we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.We obtain a namespace for abstract types that is global, i.e. meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.
- By Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar and Rok Strniša.
- To be presented at ICFP 2007.
- Download in postscript or pdf.
-
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 &emdash; usually either LaTeX for informal mathematics, or the formal mathematics of a proof assistant &emdash; 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 271 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.
- By Scott Owens and Gilles Peskine.
- To be presented at WMM 2007.
- Download in pdf.