Coinductive (applicative) characterizations of various observational congruences which arise in the semantics of λ-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.
CITATION STYLE
Lenisa, M. (1997). Semantic techniques for deriving coinductive characterizations of observational equivalences for λ-calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1210, pp. 248–266). Springer Verlag. https://doi.org/10.1007/3-540-62688-3_40
Mendeley helps you to discover research relevant for your work.