Linear lambda calculi

Following is the list of references I know of that deal with lambda
calculi based on linear logic.  If you know of updates or additions to
the list, I'd be grateful if you pass them on to me.

I do not know of a reference that shows that any of these calculi
possess the Church-Rosser property.  Again, I'd be grateful for
enlightenment (or confirmation).

Cheers,  -- P

S. Abramsky,
Computational interpretations of linear logic.
{\em Theoretical Computer Science\/} 111:3--57, 1993.

N. Benton, G. Bierman, V. de Paiva, and M. Hyland,
Type assignment for intuitionistic linear logic.
Draft paper, August 1992.

J. Chirimar, C. A. Gunter, and J. G. Riecke.
Linear ML.  In {\em Symposium on Lisp and Functional Programming},
ACM Press, San Francisco, June 1992.

S. Holmstr\"om,
A linear functional language.
Draft paper, Chalmers University of Technology, 1988.

Y. Lafont,
The linear abstract machine.
{\em Theoretical Computer Science}, 59:157--180, 1988.

P. Lincoln and J. Mitchell,
Operational aspects of linear lambda calculus.
{\em 7'th Symposium on Logic in Computer Science},
Santa Cruz, California, June 1992.  IEEE Press.

I. Mackie,
Lilac: a functional programming language based on linear logic.
Master's Thesis, Imperial College London, 1991.

A. S. Troelstra,
{\em Lectures on Linear Logic}.
CSLI Lecture Notes, 1992.

P. Wadler,
Linear types can change the world!
In M.~Broy and C.~Jones, editors, {\em Programming Concepts
and Methods}, Sea of Galilee, Israel, North Holland, April 1990.

P. Wadler,
A syntax for linear logic.
{\em Ninth International Conference on the
Mathematical Foundations of Programming Semantics},
New Orleans, Lousiana, April 1993.  Springer Verlag, LNCS 802.

P. Wadler,
A taste of linear logic.
{\em Mathematical Foundations of Computer Science},
Gdansk, Poland, August 1993.  Springer Verlag, LNCS 711.