### A terminating and confluent linear lambda calculus.

Yo Ohta and Masahito Hasegawa

In Proc. 17th International Conference on Rewriting Techniques and Applications (RTA'06), Seattle.
Springer LNCS 4098, pages 166-180, August 2006.

### Correction (November 2006)

The paper in the conference proceedings contains various small technical flows, and a very serious one - there is a missing rewrite rule:
```  \z.(let !y be M in let !x be L in N) > let !x be L in \z.(let !y be M in N)
```
where z is *free* in M. Without this rule, the system is not locally confluent/coherent modulo the equivalence relation \sim^*. In particular, Lemma 1 in the paper fails. For example, consider
```M  = \z.(let !x be L in let !y be M in N)
M1 = \z.(let !y be M in let !x be L in N)
M2 = let !x be L in \z.(let !y be M in N)
```
where x is not free in M, and z is free in M. Then M \sim M1 and M > M2 (via the rule com3), but in general M1 and M2 are not joinable modulo \sim^*, due to the side condition on com3.

After adding this rule, all the results in the paper are indeed valid.