• DocumentCode
    2894390
  • Title

    The Church-Rosser property for βη-reduction in typed λ-calculi

  • Author

    Geuvers, Herman

  • Author_Institution
    Fac. of Math. & Comput. Sci., Nijmegen Univ., Netherlands
  • fYear
    1992
  • fDate
    22-25 Jun 1992
  • Firstpage
    453
  • Lastpage
    460
  • Abstract
    The Church-Rosser property (CR) for pure type systems with βη-reduction is investigated. It is proved that CR (for βη) on the well-typed terms of a fixed type holds, which is the maximum one can expect in view of Nederpelt´s (1973) counterexample. The proof is given for a large class of pure type systems that contains, e.g., LF F, Fω, and the calculus of constructions
  • Keywords
    data structures; formal logic; Church-Rosser property; beta eta -reduction; calculus of constructions; lambda calculus; pure type systems; typed lambda -calculi; Calculus; Chromium; Computer science; Lapping; Mathematics; Reactive power; Time of arrival estimation;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
  • Conference_Location
    Santa Cruz, CA
  • Print_ISBN
    0-8186-2735-2
  • Type

    conf

  • DOI
    10.1109/LICS.1992.185556
  • Filename
    185556
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2894390