Confluence Results

  • Roberto Di Cosmo
Part of the Progress in Theoretical Computer Science book series (PTCS)


In the λ-calculus there are plenty of programs (or λ-terms) where it is pos­sible to apply the reduction rule β, introduced in 1.3.4, in more than one position. The λ-calculus does not specify a unique evaluation order, or reduction strategy, that associates to each program or term a unique position where the reduction will proceed.


Coherence Assure Rosen Prep Lost 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Birkhäuser Boston 1995

Authors and Affiliations

  • Roberto Di Cosmo
    • 1
  1. 1.Ecole Normale SupérieureLIENS-DMIParis Cedex 05France

Personalised recommendations