Abstract
We give a simple characterization of convergent terms in Abadi and Cardelli untyped Object Calculus (\( \varsigma \) -calculus) via intersection types. We consider a λ-calculus with records and its intersection type assignment system. We prove that convergent λ-terms are characterized by their types. The characterization is then inherited by the object calculus via self-application interpretation.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, A Theory of Objects, Springer 1996.
M. Abadi, L. Cardelli, R. Viswanathan, “An interpretation of objects and object types” Proc. of of POPL’96 1996, 396–409.
S. Abramsky, “Domain Theory in Logical Form”, APAL 51, 1991, 1–77.
S. Abramsky, C.-H. L. Ong “Full abstraction in the lazy lambda calculus”, Inf. Comput. 105(2), 1993, 159–267.
S. van Bakel, Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting, Ph.D. Thesis, Mathematisch Centrum, Amsterdam 1993.
H.P. Barendregt, M. Coppo, M. Dezani, “A Filter Lambda Model and the Completeness of Type Assignment”, JSL 48, 1983, 931–940.
G. Boudol, “A Lambda Calculus for (Strict) Parallel Functions”, Info. Comp. 108, 1994, 51–127.
K.B. Bruce, “A paradigmatic Object-Oriented design, static typing and semantics”, J. of Fun. Prog. 1(4), 1994, 127–206.
K.B. Bruce, L. Cardelli, B.C. Pierce, “Comparing object encodings”, Proc. of TACS’97, LNCS 1281, 1997, 415–438.
K. Crary, “Simple, Efficient Object Encoding using Intersection Types”, CMU Technical Report CMU-CS-99-100.
M. Coppo, F. Damiani, P. Giannini, “Inference based analyses of functional programs: dead-code and strictness”, in M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998 [28]}, 143–176.
M. Coppo, M. Dezani, B. Venneri, “Functional characters of solvable terms”, Grund. der Math., 27, 1981, 45–58.
M. Coppo, A. Ferrari, “Type inference, abstract interpretation and strictness analysis”, TCS 121, 1993, 113–144.
M. Dezani, E. Giovannetti, U. de Liguoro, “Intersection types, λ-models and Böhm trees”, in M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998 [28]}, 45–97.
M. Dezani, F. Honsell, Y. Motohama, “Compositional Characterizations of λ-terms using Intersection Types”, Proc. of MFCS’00, LNCS 1893, 2000, 304–313.
M. Dezani, U. de Liguoro, A. Piperno. “A filter model for concurrent lambda-calculus”, Siam J. Comput. 27(5), 1998, 1376–1419.
L. Egidi, F. Honsell, S. Ronchi della Rocca, “Operational, denotational and logical descriptions: a case study”, Fund. Inf. 16, 1992, 149–169.
K. Fisher, F. Honsell, J.C. Mitchell, “A lambda calculus of objects and method specialization”, Nordic J. Comput. 1, 1994, 3–37.
A. Gordon, G. Rees, “Bisimilarity for first-order calculus of objects with subtyping”, Proc. of POPL’96, 1996, 386–395.
H. Ishihara, T. Kurata, “Completeness of intersection and union type assignment systems for call-by-value λ-models”, to appear in TCS.
S. Kamin, “Inheritance in Smalltalk-80: a denotational definition”, Proc. of POPL’88, 1988, 80–87.
J.L. Krivine, Lambda-calcul, types et modéles, Masson 1990.
J.C. Mitchell, Foundations for Programming Languages, MIT Press, 1996.
B. Pierce, Programming with Intersection Types and Bounded Polymorphism, Ph.D. Thesis, 1991.
G. Pottinger, “A Type Assignment System for Strongly Normalizable λ-terms”, in R. Hindley, J. Seldin eds., To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalisms, Academic Press, 1980, 561–527.
J. Reynolds, “The Coherence of Languages with Intersection Types”, LNCS 526, 1991, 675–700.
D. Scott, “Data types as lattices”, SIAM J. Comput. 5,n. 3, 1976, 522–587.
M. Takahashi, M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de’Liguoro, U. (2001). Characterizing Convergent Terms in Object Calculi via Intersection Types. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_25
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive