John C. Mitchell
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.
- {Bruce and Meyer 84} Bruce, K. and Meyer, A., A Completeness Theorem for Second-Order Polymorphic Lambda Calculus. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), 1984, pages 131--144. Google Scholar
Digital Library
- {Bruce, Meyer and Mitchell 85} Bruce, K. B., Meyer, A. R. and Mitchell, J. C., The semantics of second-order lambda calculus to appearGoogle Scholar
- {Burstall and Lampson 84} Burstall, R. and Lampson, B., A Kernel Language for Abstract Data Types and Modules. In Proc. Int'l Symp. on Semantics of Data Types, 1984, pages 1--50. Google ScholarDigital Library
- {Donahue 79} Donahue, J., On the semantics of data type. SIAM J. Computing 8 1979. pages 546--560Google Scholar
- {Friedman 75} Friedman, H., Equality Between Functionals. In R. Parikh (ed.), Logic Colloquium, pages 22--37. Springer-Verlag 1975.Google Scholar
- {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<sup>nd</sup> Scandinavian Logic Symp., pages 63--92. North-Holland 1971.Google Scholar
- {Gordon, et. al. 79} Gordon, M. J., R. Milner and C. P. Wadsworth, Edinburgh LCF. Lecture Notes in Computer Science, Vol. 78 Springer-Verlag 1979.Google Scholar
- {Haynes 84} Haynes, C. T., A Theory of Data Type Representation Independence. In Int. Symp. on Semantics of Data Types, Springer-Verlag, 1984, pages 157--176. Google ScholarDigital Library
- {Liskov et. al. 81} Liskov, B. et. al., CLU Reference Manual. Lecture Notes in Computer Science, Vol. 114 Springer-Verlag 1981. Google ScholarDigital Library
- {MacQueen 85} MacQueen, D. B., Modules for Standard ML. Polymorphism 2, 2 1985. 35 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming. Google ScholarDigital Library
- {MacQueen 86} MacQueen, D. B., Using dependent types to express modular structure. In Proc. 13-th ACM Symp. on Principles of Programming Languages, 1986. To appear. Google ScholarDigital Library
- {Martin-L&ouml;f 79} Martin-L&ouml;f, P., Constructive mathematics and computer programming. 1979. Paper presented at 6<sup>th</sup> International Congress for Logic, Methodology and Philosophy of Science, Preprint, Univ. of Stockholm, Dept. of Math. 1979Google Scholar
- {McCraken 79} McCracken, N., An Investigation of a Programming Language with a Polymorphic Type Structure. Syracuse Univ. 1979. Google ScholarDigital Library
- {Milner 85} Milner, R., The standard ML core language. Polymorphism 2, 2 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.Google Scholar
- {Mitchell 84c} Mitchell, J. C., Semantic models for second-order lambda calculus. In Proc. 25-th IEEE Symp. on Foundations of Computer Science, 1984, pages 289--299.Google ScholarDigital Library
- {Mitchell and Plotkin 85} Mitchell, J. C. and Plotkin, G. D., Abstract types have existential types. In Proc. 12-th ACM Symp. on Principles of Programming Languages, January, 1985. pp. 37--51. Google ScholarDigital Library
- {Mitchell and Meyer 85} Mitchell, J. C. and Meyer, A. R., Second-order logical relations. In Logics of Programs, June, 1985. pages 225--236. Google ScholarDigital Library
- {Plotkin 80} Plotkin, G. D., Lambda definability in the full type hierarchy. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363--373. Academic Press 1980.Google Scholar
- {Reynolds 74} Reynolds, J. C., Towards a Theory of Type Structure. In Paris Colloq. on Programming, Springer-Verlag, 1974, pages 408--425. Google ScholarDigital Library
- {Reynolds 83} Reynolds, J. C., Types, Abstraction, and Parametric Polymorphism. In IFIP Congress, 1983.Google Scholar
- {Statman 82} Statman, R., Logical relations and the typed lambda calculus. (Manuscript.) To appear in Information and Control.Google Scholar
- {Tait 67} Tait, W. W., Intensional interpretation of functionals of finite type. J. Symbolic Logic 32 1967. pages 198--212Google Scholar
- Representation independence and data abstraction
Recommendations
Internalizing representation independence with univalence
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language ...
On understanding types, data abstraction, and polymorphism
The MIT Press scientific computation seriesOur objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the relevance of recent research to the design of practical ...
State-dependent representation independence
POPL '09Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity -- two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation ...
Comments