Regrettably, there are several typos in this paper. For most, our intended meaning is still clear. However, some of them may be confusing, and thus are worth mentioning. They are:
In Figure 2, the "canlam" rule is upside-down.
In Figure 3, the "convlam" rule is upside-down.
In the last sentence before Section 3.2, the word "eigenvalues" should be replaced with "eigenvariables."
In Figure 5, in the premiss in the rule "hascnwh," "M0 -->wh N0" should be replaced with "whr M0 N0".
In Theorem 5.1, the last line of the second case for IH (1) should be replaced with the following two lines:
Phi => P(M x) by IH (1)
Phi => P(M) by ad1
and the third "step" in the second case for IH (2) should be deleted.
In corollary 6.1, "where hascnwh is of the form ad3" should read "where ad3 is admissible by the soundness of whr and the rule hascnwh."
In Theorem 7.1, the "J" in "for some judgment J" should be in a different font.
In corollary 7.1, "rule hascnwh" should read "the soundness of whr and the rule hascnwh".
We apologize of these errors.

The current relesae version of the implementation is lr.tgz version 0.9. Although the files here aren't 100% consistent in terms of naming convention, etc., the files are better commented, and the structure of the proof more closely matches that of the paper.
Last updated 2/15/2005 at 5:28pm.