🚀 go-pugleaf

Date: Tue, 15 Sep 1992 11:23:20 +0100 (BST)

Here is the reference to a paper describing my work on the lazy lambda
calculus which Jean-Yves alluded to in his message:
``The lazy lambda calculus'' in Research Topics in Functional
Programming, ed. D. Turner, Addison Wesley 1990, pages 65-117.
There is also a joint paper with Luke Ong on ``Full Abstraction in
theLazy lambda Calculus'', which is to appear in Information and
Computation next year. It is currently available as a U. Cambridge
Computer laboratory report (No. 259).

On the matter of different translations of lambda calculus, it might be
worth mentioning that it is the one based on the recursive type 
	D = !(D -o D)
and NOT 
	D = !D -o D,
which is used by Gonthier, Abadi and Levy in their ``rational
reconstruction'' of Lamping's algorithm for optimal reduction in the
lambda calculus.  (See their POPL paper of this year). The former
translation seems to allow more sharing than the latter.

This seems to me to be an excellent example of the way in which the
finer-grained Linear connectives allow important operational
distinctions to be reflected in the logic, and studied in a structural
way.

Samson Abramsky