SHARING IN THE WEAK LAMBDA-CALCULUS REVISITED
Tomasz Blanc, Jean-Jacques L ́ Evy, Luc Maranget · 2007
Abstract. In a previous paper [2] 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 [11]. 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 [2]. 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