Cited By
View all- Howe DStoller S(2005)An operational approach to combining classical set theory and functional programming languagesTheoretical Aspects of Computer Software10.1007/3-540-57887-0_89(36-55)Online publication date: 31-May-2005
On extending computational adequacy by data abstraction
Pages 161 - 169
Abstract
Given an abstract data type(ADT), and algebra that specifies it, and an implementation of the data type in a certain language, if the implementation is “correct,” a certain principle of modularity of reasoning holds. Namely, one can safely reason about programs in the language extended by the ADT, by interpreting the ADT operation symbols according to the specification algebra. The main point of this paper is to formalize correctness as a local condition involving only the specification and the implementation and to prove the equivalence of such a condition to the modularity principle. We conduct our study in the context of a language without divergence (in subsection 2.1), and for languages with divergence and general recursion (in subsections 2.2 and 2.3). We also describe a sufficient condition under which, given an implementation, there may be a finite set of observational equivalences which imply the local condition. Further, we illustrate a technique for proving in a practical situation that a given implementation of an abstract data type is correct.
References
[1]
S. Abramsky. Abstract Interpretation, Logical Relations, and Kan Extensions. J. Logic and Computation, 1, 1990.
[2]
R. M. Amadio. A Fixed Point Extension of the Second-Order Lambda Calculus: Observable Equivalences and Models. In Proceedings of the Symposium on Logic in Computer Science, pages 51-60. IEEE, July 1988.
[3]
J. Donahue. On the Semantics of Data Type. SIAM J. Computing, 8:546-560, 1979.
[4]
H. Friedman. Equality between Functionals. In R. Parikh, editor, Proceedings of the Logic Colloqium '73, pages 22-37. Lecture Notes in Mathematics, Vol. 453, Spfinger-Vefiag, 1975.
[5]
C. T. Haynes. A Theory of Data Type Representation Independence. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Proceedings of the Conference on Semantics of Data Types, Sophia-Antipolis, June 198J, pages 157-176. Lecture Notes in Computer Science, Vol. 173, Springer- Verlag, 1984.
[6]
R. Harper, J. C. Mitchell, and E. Moggi. Higher-order Modules and the Phase Distinction. In Principles of Programming Languages, pages 341- 354, January 1990.
[7]
D. B. MacQueen. Using Dependent Types to Express Modular Structure. In Conf. Record Thirteenth Ann. Syrup. Principles of Programming Languages, pages 277-286. ACM, January 1986.
[8]
A.R. Meyer and S. S. Cosmadakis. Semantical Paradigms: Notes for an Invited Lecture. In Proceedings of the Symposium on Logic in Computer Science, pages 236-255. IEEE, July 1988.
[9]
J.C. Mitchell. Representation Independence and Data Abstraction. In Proceedings of the 13th Symposium on Principles of Programming Languages, pages 263-276. ACM, January 1986.
[10]
J.C. Mitchell and A. R. Meyer. Secondorder logical relations (extended abstract). In R. Parikh, editor, Proceedings of the Conference on Logics of Programs, Brooklyn, June 1985, pages 225-236. Lecture Notes in Computer Science, Vol. 193, Springer-Verlag, 1985.
[11]
J.C. Mitchell and G. D. Plotkin. Abstract Types have Existential Type. In Proceedings of the 12th Symposium on Principles of Programming Languages, pages 37-51. ACM, January 1985.
[12]
G.D. Plotkin. LCF Considered as a Programming Language. Theoretical Computer Science, 5(3):223-256, December 1977.
[13]
G.D. Plotkin. 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.
[14]
J.C. Reynolds. Towards a Theory of Type Structure. In B. Robinet, editor, Programming Symposium, pages 408- 425. Springer Lecture Notes in Computer Science, Vol. 19, Springer-Verlag, 1974.
[15]
J.C. Reynolds. Types, Abstraction, and Parametric Polymorphism. In R. E. A. Mason, editor, Information Processing '83, pages 513-523. North- Holland, 1983.
[16]
R. Statman. Logical Relations and the Typed A-calcuhs. Information and Control, 65:85-97, 1985.
Index Terms
- On extending computational adequacy by data abstraction
Recommendations
On extending computational adequacy by data abstraction
Given an abstract data type(ADT), and algebra that specifies it, and an implementation of the data type in a certain language, if the implementation is “correct,” a certain principle of modularity of reasoning holds. Namely, one can safely reason about ...
On the power of coercion abstraction
POPL '12Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 1992 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 January 1992
Check for updates
Qualifiers
- Article
Conference
LFP92: ACM Conference on Lisp and Functional Programming
June 22 - 24, 1992
California, San Francisco, USA
Acceptance Rates
Overall Acceptance Rate 30 of 109 submissions, 28%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 321Total Downloads
- Downloads (Last 12 months)64
- Downloads (Last 6 weeks)16
Reflects downloads up to 02 Mar 2025
Other Metrics
Citations
Cited By
View all- Howe DStoller S(2005)An operational approach to combining classical set theory and functional programming languagesTheoretical Aspects of Computer Software10.1007/3-540-57887-0_89(36-55)Online publication date: 31-May-2005
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in