Nordic Journal of Computing Bibliography

Abstract

The metavariable self is fundamental in object-oriented languages. Typing self in the presence of inheritance has been studied by Abadi and Cardelli, Bruce, and others. A key concept in these developments is the notion of selftype, which enables flexible type annotations that are impossible with recursive types and subtyping. Bruce et al. demonstrated that, for the language TOOPLE, type checking is decidable. Open until now is the problem of type inference with selftype. In this paper we present a simple type system with selftype, recursive types, and subtyping, and we prove that type inference is NP-complete. With recursive types and subtyping alone, type inference is known to be P-complete.Our example language is the object calculus of Abadi and Cardelli. Both our type inference algorithm and our lower bound are the first such results for a type system with selftype.

Categories and Subject Descriptors: D.3.2 [Programming Languages]: Language Classifications; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs

Additional Key Words and Phrases: type inference, constraints

Selected references

• Martín Abadi and Luca Cardelli. A theory of primitive objects - untyped and first-order systems. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software: International Symposium, volume 789 of Lecture Notes in Computer Science, pages 296-320. Springer-Verlag, April 1994.

• Kim B. Bruce. Safe type checking in a statically-typed object-oriented programming language. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 285-298, Charleston, South Carolina, January 1993.

• William Cook and Jens Palsberg. A denotational semantics of inheritance and its correctness. In Norman Meyrowitz, editor, Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA'89), pages 433-443, New Orleans, Louisiana, 1-6 October 1989. SIGPLAN Notices, 24(10), October 1989.

• Kathleen Fisher, Furio Honsell, and John C. Mitchell. A lambda calculus of objects and method specialization. Nordic Journal of Computing, 1(1):3-37, Spring 1994.

• My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 176-185, San Francisco, California, January 1995.

• John C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 109-124, San Francisco, California, January 1990.

• Jens Palsberg. Efficient inference of object types. Information and Computation, 123(2):198-209, December 1995.

• Jens Palsberg and Michael I. Schwartzbach. Static typing for object-oriented programming. Science of Computer Programming, 23(1):19-53, October 1994.

• Jerzy Tiuryn. Subtype inequalities. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 308-315, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.

• Sergei G. Vorobyov. Structural decidable extensions of bounded quantification. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 164-175, San Francisco, California, January 1995.

Shortcuts: