This directory accompanies the paper:

  _Run Your Research: On the Effectiveness of Lightweight
  Mechanization_ by Casey Klein, John Clements, Christos Dimoulas,
  Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy,
  Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler

It contains the models that we used when testing the papers from ICFP
2009, with the below giving an overview of how big the models are, how
many test cases we wrote for each model (note that these test cases
count anything that we tested related to the model, not just tests of
what was written in the corresponding paper; for example, they contain
test cases for substitution functions (when appropriate)), how many
properties we tested randomly, and the names of the properties.

3: 
  Test cases: 67
  Loc: 2458
  Randomly tested properties: (as described in the paper)

  This model is included with the Racket distribution and the counts
  are as of the 5.2 release of Racket.

4.1:
  Test cases: 24
  Loc: 1196
  Randomly tested properties: 1

  1. Agda implementation matches Redex implementation of
     the rules given the paper.

4.2:
  Test cases: 10
  Loc: 849
  Randomly tested properties: 5

  1. The normalization relation is a function.
  2. Normalization actually produces normal forms.
  3. The relation ↦ is single-valued.
  4. Normalization preserves types.
  5. Normalization preserves meaning.

4.3:
  Test cases: 32
  Loc: 1197
  Randomly tested properties: 5

  1. Unique decomposition.
  2. Sequential steps reduce in any E context.
  3. If there is potential communication, the term is reducible.
  4. The result of a program with memoization enabled is the same as
     with memoization disbaled.
  5. Safety theorem (section 5).

4.4:
  Test cases: 55
  Loc: 1445
  Randomly tested properties: 4

  1. Compilation preserves ~
  2. Freshly compiled terms satisfy invariance
  3. The compiled version of an irreducible term
     also does not reduce
  4. If a compiled term does not contain an in/out matched pair,
     then compilation preserves ~ (a refinement of #1)

4.5:
  Test cases: 105
  Loc: 1548
  Randomly tested properties: 3

  1. The decomposition used in translation is unique.
  2. The translation function has the range claimed.
  3. Translation preserves meaning.

4.6:
  Test cases: 148
  Loc: 1159
  Randomly tested properties: 8

  1. Lemma 5.1
  2. Lemma 4.1
  3. F = Fc (section 4 para 3)
  4. Lemma 4.2
  5. Theorem 4.1
  6. Abstract interpretation matches evaluation
  7. CPS soundness
  8. Theorem 5.1

4.7:
  Test cases: 97
  Loc: 1223
  Randomly tested properties: 5

  1. The type system is sound.
  2. Compilation preserves meaning.
  3. Their semantics produces the same answer as Racket.
  4. A-normalization preserves types.
  5. CPS-conversion produces a well-typed expression.

4.8:
  Test cases: 57
  Loc: 1335
  Randomly tested properties: 3

  1. Theorem 1.
  2. Theorem 2.
  3. Theorem 11.

4.9: not signed off (Carl) 
  Test cases: 67
  Loc: 1143
  Randomly tested properties: 1

  1. Type soundness.
