This repository contains an attempt to find the unsoundness motivating the value restriction [1] automatically, using the Korat test generation tool [2].

The `letref' directory contains a Java interpreter for an unsound language with let-polymorphism and ref cells.

The `testgen' directory contains a Korat configuration that searches for the bug. To run it:

1. Download Korat from this URL:

   http://sourceforge.net/projects/korat/files/korat/korat-1.0/korat-all-1.0.zip

2. Unzip it into this directory.

3. Compile everything:

   javac -cp korat/korat.jar:. testgen/.java letref/.java

4. Invoke Korat:

   java -cp korat/korat.jar:. korat.Korat \ --class testgen.TestInput \ --args 1,1,letref.Lam:2:1 \ --progress 1000000 \ --listeners testgen.TestExec

The three comma-delimited --args arguments control the space of test inputs that Korat will explore. The first and second arguments respectively bound the number of distinct variables and integers that Korat may use to construct each test input. The third argument limits the number of objects of each of the other Expr classes, except Bool, which may be used freely. These objects appear at most once in the test input's object graph. For example, the expression:

((lam (x) x) (lam (x) x))

requires two Lam objects. The third argument takes one of two forms:

1. a natural number applying to all of the other Expr implementations,

2. a string of the form letref.[C]:[c]:[n], configuring the search space to include tests inputs comprising [c] objects of class [C] and [n] objects of each of the other Expr implementations.

Running with the sample arguments above finds this bug-revealing expression:

((! (let (x0 (ref (lam (x0) 0))) (seq (x0 := (lam (x0) (+1 x0))) x0))) true)

It takes just under two hours on my machine.

[1] http://www.ccs.neu.edu/scheme/pubs/lasc95-w.ps.gz [2] http://korat.sourceforge.net/