Paths in the lambda-calculus. Three years of communications without understanding

A Asperti, V. Danos, C. Laneve, L. Regnier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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
Original languageEnglish
Title of host publicationLogic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages11
ISBN (Print)0-8186-6310-3
Publication statusPublished - Jul 1994

Keywords / Materials (for Non-textual outputs)

  • computational geometry
  • graph theory
  • lambda calculus
  • β-reduction
  • consistent paths
  • graph-reduction algorithm
  • interaction geometry
  • labeled reductions
  • lambda-calculus
  • legal paths
  • redex families
  • regular paths
  • Algorithm design and analysis
  • Displays
  • Geometry
  • Joining processes
  • Law
  • Legal factors
  • Logic devices


Dive into the research topics of 'Paths in the lambda-calculus. Three years of communications without understanding'. Together they form a unique fingerprint.

Cite this