Abstract:
Sangiorgi has shown that the semantics induced by Milner's encoding of the call-by-name lambda-calculus in the pi-calculus is the equality of Lévy-Longo trees. Later it was realized that Milner's encodings are actually variations on well-known continuation passing style transforms. Then a question is: is the discriminating ability due to pi-calculus features, or is it already offered by the CPS transform? We show that the latter is true: the semantics induced by the call-by-name CPS transform on lambda-terms is Lévy-Longo trees equality.