The proof of the Jack-of-All-Trades Principle is wrong. See the pdf
for a problem with it.
Thanks to James T. Perconti for uncovering the
bug and alerting us to it.
This directory contains a Redex model for the POPL 2011 paper _Blame |
for All_ by Ahmed, Findler, Siek, and Wadler. |
It requires at least Racket version 5.0.99.2, available at |
| http://www.racket-lang.org/ |
Modelled are: |
- the operational semantics and type system from figure 1 |
- the operational semantics and type system from figure 3, |
- the operational semantics that combines figures 1, 3, and 4, |
- the subtype relation <: from figure 5, and |
- the sf<: relation from figure 7. |
In addition there are a few hundred test cases that help ensure that |
stupid mistakes don't happen. Many of them just test that the Redex |
model behaves as expected, but there are also tests that check type |
preservation and sf<: preservation for entire reduction sequences. |
----------------------------------------------------------------------------- |
There are a few changes from what is shown in the paper to the Redex |
model in order to accomodate Redex's status as a (fancy) functional |
programming language. |
1: The notation used in the model is changed systematically from that |
in the paper. Specifically: |
a) Parentheses are always at the beginning and ending of each |
production in the grammar (following Scheme/Lisp tradition) |
unlike in the paper where they sometimes appear in the middle of |
a production; |
b) All of the commas and periods are dropped |
c) The vertical bar over variables is written (bar x) or (bar X) |
d) The latex \rightarrow is written as ->. |
e) The latex \star is written as *. |
f) Other punctuation and metavariables uses unicode characters, |
e.g. ⇒, ν, and Γ (the type arrow, \nu, and \Gamma). |
2: the term 'blame p' is annotated with its type. |
3: the second to last rule in in the definition of A <: B is not given |
in its full generality; instead, just a few versions of it for |
specific C's is given (since Redex cannot "guess" witness types to |
satisfy the rule). |
----------------------------------------------------------------------------- |
The files here are: |
README: this file |
stlc.rkt: contents of figure 1 |
stlc-test.rkt: tests for the above |
nu.rkt: contents of figure 3 |
nu-test.rkt: tests for the above |
contract-nu.rkt: contents of figure 4 |
contract-nu-test.rkt: tests for the above |
combined-test.rkt: runs the stlc tests in the nu system |
same-ty.rkt: a library of functions on types |
same-ty-test.rkt: tests for the above |
preservation.rkt: a library for testing preservation of some subject |
all-tests.rkt: runs all of the tests |