Sharing in the Weak Lambda-Calculus Revisited

Tomasz Blanc
INRIA

Jean-Jacques Lévy
INRIA, Microsoft Research-INRIA Joint Centre

Luc Maranget
INRIA

Abstract

In a previous paper [4] which appeared in the volume celebrating Klop’s 60th anniversary, we presented a labeled lambda-calculus to characterize the dag implementation of the weak lambda-calculus as described in Wadsworth’s dissertation [14]. In this paper, we simplify this calculus and present a simpler proof of the sharing property which allows the dag implementation. In order to avoid duplication of presentations, we mainly show here the modifications brought to the weak labeled lambda-calculus in [4]. The reader is therefore recommended to read first the companion article and later read our present paper. We are happy that this note can therefore be considered as establishing a new bridge between two friends and now senior colleagues, Jan Willem Klop and Henk Barendregt whom this work is dedicated to on the occasion of his 60th birthday.

Full text

PDF