Representation independence and data abstraction

ABSTRACT

One purpose of type checking in programming languages is to guarantee a degree of "representation independence:" programs should not depend on the way stacks are represented, only on the behavior of stacks with respect to push and pop operations. In languages with abstract data type declarations, representation independence should hold for user-defined types as well as built-in types. We study the representation independence properties of a typed functional language (second-order lambda calculus) with polymorphic functions and abstract data type declarations in which data type implementations (packages) may be passed as function parameters and returned as results. The type checking rules of the language guarantee that two data type implementations P and Q are equivalence whenever there is a correspondence between the behavior of the operations of P and the behavior of the operations of Q.

REFERENCES

• 1: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 2: {Bruce, Meyer and Mitchell 85} Bruce, K. B., Meyer, A. R. and Mitchell, J. C., The semantics of second-order lambda calculus to appear
• 3: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 4: {Donahue 79} Donahue, J., On the semantics of data type. <i>SIAM J. Computing</i> 8 1979. pages 546--560
• 5: {Friedman 75} Friedman, H., Equality Between Functionals. In R. Parikh (ed.), <i>Logic Colloquium,</i> pages 22--37. Springer-Verlag 1975.
• 6: {Girard 71} Girard, J.-Y., Une extension de l'interpretation de G&ouml;del &agrave; l'analyse, et son application &agrave; l'&eacute;limination des coupures dans l'analyse et la th&eacute;orie des types. In Fenstad, J. E. (ed.), 2<i>^nd Scandinavian Logic Symp.,</i> pages 63--92. North-Holland 1971.
• 7: {Gordon, et. al. 79} Gordon, M. J., R. Milner and C. P. Wadsworth, <i>Edinburgh LCF.</i> Lecture Notes in Computer Science, Vol. 78 Springer-Verlag 1979.
• 8: Christopher T. Haynes, A theory of data type representation independence., Proc. of the international symposium on Semantics of data types, p.157-175, July 1984, Sophia-Antipolis, France
• 9: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 10: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 11: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 12: {Martin-L&ouml;f 79} Martin-L&ouml;f, P., Constructive mathematics and computer programming. 1979. Paper presented at 6^th International Congress for Logic, Methodology and Philosophy of Science, Preprint, Univ. of Stockholm, Dept. of Math. 1979
• 13: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 14: {Milner 85} Milner, R., The standard ML core language. <i>Polymorphism</i> 2, 2 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.
• 15: {Mitchell 84c} Mitchell, J. C., Semantic models for second-order lambda calculus. In <i>Proc. 25-th IEEE Symp. on Foundations of Computer Science,</i> 1984, pages 289--299.
• 16: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential types, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.37-51, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318606]
• 17: John C. Mitchell , Albert R. Meyer, Second-Order Logical Relations (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.225-236, June 17-19, 1985
• 18: {Plotkin 80} Plotkin, G. D., Lambda definability in the full type hierarchy. In <i>To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,</i> pages 363--373. Academic Press 1980.
• 19: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 20: {Reynolds 83} Reynolds, J. C., Types, Abstraction, and Parametric Polymorphism. In <i>IFIP Congress,</i> 1983.
• 21: {Statman 82} Statman, R., Logical relations and the typed lambda calculus. (Manuscript.) To appear in Information and Control.
• 22: {Tait 67} Tait, W. W., Intensional interpretation of functionals of finite type. <i>J. Symbolic Logic</i> 32 1967. pages 198--212