Abstract
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.
Work supported by CNR, EC HCM Project No. CHRX-CT92.0046 Lambda-Calcul Typé, and MURST 40% grant.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky, L. Ong, Full Abstraction in the Lazy Lambda Calculus, Information and Computation, 105(2):159–267, 1993.
H. Barendregt, The Lambda Calculus, its Syntax and Semantics, North Holland, Amsterdam, 1984.
H. Barendregt, M. Coppo, M. Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, J.Symbolic Logic, 48(4):931–940, 1983.
M. Coppo, M. Dezani-Ciancaglini, M. Zacchi, Type Theories, Normal Forms and D∞-Lambda-Models, Information and Computation, 72(2):85–116, 1987.
L. Egidi, F. Honsell, S. Ronchi Della Rocca, Operational, denotational and logical Descriptions: a Case Study, Rundamenta Informaticae, 16(2):149–169, 1992.
P. Freyd, Algebraically complete categories, A.Carboni et al. eds, Category Theory '90 Springer LNM, 1488:95–104, Como, 1990.
F. Honsell, M. Lenisa, Some Results on Restricted λ-calculi, MFCS'93 Conference Proceedings, A.Borzyszkowski et al. eds., Springer LNCS, 711:84–104, 1993.
F. Honsell, M. Lenisa, Final Semantics for untyped λ-calculus, M.Dezani et al. eds, TLCA'95 Springer LNCS, 902:249–265, Edinburgh, 1995.
F. Honsell, M. Lenisa, A Semantical Analysis of an Effective Perpetual Strategy, Draft, November 1996.
F. Honsell, S.Ronchi Della Rocca, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, J. of Computer and System Sciences, 45(1):49–75, 1992.
D. Howe, Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, 124(2):103–112, 1996.
M. Hyland, A survey of some useful partial order relations on terms of the lambdacalculus, C.Böhm ed., Springer LNCS, 37:83–95, 1975.
M. Lenisa, Final Semantics for a Higher Order Concurrent Language, CAAP'96 Conference Proceedings, H.Kirchner ed., Springer LNCS, 1059:102–118, 1996.
M. Lenisa, The Congruence Candidate Method for Giving Coinductive Characterizations of Observational Equivalences in λ-calculi, to appear in CAAP'97 Proc.
I. Mason, S. Smith, C. Talcott, From Operational Semantics to Domain Theory, Information and Computation to appear.
A.M. Pitts, Computational Adequacy via ‘Mixed’ Inductive Definitions, MFPS'93, Brookes et al. eds., Springer LNCS, 802:72–82, 1994.
A.M. Pitts, A Note on Logical Relations Between Semantics and Syntax, to appear in WoLLIC'96 Proc., J. of the Interest Group in Pure and Applied Logics.
A.M. Pitts, Relational Properties of Domains, Information and Computation, 127:66–90, 1996.
G.D. Plotkin, Call-by-name, Call-by-value and the λ-calculus, Theoretical Computer Science 1:125–159, 1975.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lenisa, M. (1997). Semantic techniques for deriving coinductive characterizations of observational equivalences for λ-calculi. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_40
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive