Return-Path: Received: from RI.CMU.EDU by POP.CS.CMU.EDU id aa29850; 11 Jul 94 9:15:17 EDT Received: from THEORY.LCS.MIT.EDU by RI.CMU.EDU id aa13006; 11 Jul 94 9:06:49 EDT Received: from vanuata.dcs.gla.ac.uk by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA03035; Mon, 11 Jul 94 08:38:33 EDT Resent-Message-Id: <199407111238.AA03035@theory.lcs.mit.edu> Message-Id: <199407111238.AA03035@theory.lcs.mit.edu> Received: from dcs.gla.ac.uk by goggins.dcs.gla.ac.uk id <07231-0@goggins.dcs.gla.ac.uk>; Tue, 5 Jul 1994 19:18:06 +0100 From: wadler@dcs.gla.ac.uk Subject: Linear lambda calculi Date: Tue, 5 Jul 94 19:07:57 BST To: types@dcs.gla.ac.uk, linear@cs.stanford.edu Old-Resent-From: types-request@dcs.gla.ac.uk Errors-To: types-request@dcs.gla.ac.uk Approved: types@dcs.gla.ac.uk Resent-Date: Tue, 5 Jul 1994 19:18:06 +0100 Resent-From: types@theory.lcs.mit.edu Resent-To: types-dist@theory.lcs.mit.edu 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.