Typed Lambda Calculi and Applications
Lecture Notes in Computer Science, 1997, Volume 1210/1997, 248-266, DOI: 10.1007/3-540-62688-3_40

Semantic techniques for deriving coinductive characterizations of observational equivalences for λ-calculi

Marina Lenisa

View Related Documents

Abstract

Coinductive (applicative) characterizations of various observational congruences which arise in the semantics of lambda-calculus, for various reduction strategies, are discussed. Two semantic techniques for establishing the coincidence of the applicative and the contextual equivalences are analyzed. The first is based on intersection types, the second is based on a mixed induction-coinduction principle.
Work supported by CNR, EC HCM Project No. CHRX-CT92.0046 Lambda-Calcul Typé, and MURST 40% grant.

Fulltext Preview

Image of the first page of the fulltext document