Re: About the questions by S. Courtenage

Thread View: fj.mail-lists.types

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by sa Tue, 15 Sep 1992 16:13

#21

Author: sa
Date: Tue, 15 Sep 1992 16:13

27 lines
1568 bytes

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

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads