## Paper: Paths in the lambda-calculus. Three years of communications without understanding (at LICS 1994)

**Andrea Asperti Vincent Danos Cosimo Laneve Laurent Regnier**

### Abstract

Since the rebirth of λ-calculus in the late 1960s, three major theoretical investigations of β-reduction have been undertaken: (1) Levy's (1978) analysis of families of redexes (and the associated concept of labeled reductions); (2) Lamping's (1990) graph-reduction algorithm; and (3) Girard's (1988) geometry of interaction. All three studies happened to make crucial (if not always explicit) use of the notion of a path, namely and respectively: legal paths, consistent paths and regular paths. We prove that these are equivalent to each other

### BibTeX

@InProceedings{AspertiDanosLaneveR-Pathsinthelambdacal, author = {Andrea Asperti and Vincent Danos and Cosimo Laneve and Laurent Regnier}, title = {Paths in the lambda-calculus. Three years of communications without understanding }, booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)}, year = {1994}, month = {July}, pages = {426--436}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }