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

Authors: 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}
  }