On the implementation of abstract data types by programming language constructs. (English) Zbl 0619.68025

Implementations of abstract data types are defined via enrichments of a target type. We propose to use an extended typed \(\lambda\)-calculus for enrichments in order to meet the conceptual requirement that an implementation has to bring us closer to a (functional) program. Composability of implementations is investigated, the main result being that composition of correct implementations is correct if terminating programs are implemented by terminating programs. Moreover, we provide syntactical criteria to guarantee correctness of composition. The proof is based on strong normalization and Church-Rosser results of the extended \(\lambda\)-calculus which seem to be of interest in their own right.


68P05 Data structures
Full Text: DOI


[1] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness and implementation of abstract data types, () · Zbl 0359.68018
[2] Barendregt, H., The lambda calculus, (1984), North-Holland Amsterdam · Zbl 0549.03012
[3] Berry, G.; Curien, P.L.; Levy, J.-J., Full abstraction for sequential languages: the state of the art, () · Zbl 0604.68033
[4] Blum, E.K.; Parisi-Presicce, F., Implementation of data types by algebraic methods, J. comput. system sci., 27, 304-330, (1983) · Zbl 0537.68026
[5] Broy, M.; Wirsing, M., Programming languages as abstract data types, () · Zbl 0433.68014
[6] Cartmell, J.W., Generalized algebraic theories and contextual categories, () · Zbl 0634.18003
[7] Curien, P.-L., Categorical combinators, sequential algorithms and functional programming, (1986), Pitman London · Zbl 0643.68004
[8] Ehrig, H.; Kreowski, H.-J.; Mahr, B.; Padawitz, P., Algebraic implementation of abstract data types, Theoret. comput. sci., 20, (1982) · Zbl 0483.68018
[9] Ehrig, H.; Kreowski, H.-J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B.; Kreowski, H.J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Parameter passing in algebraic specification languages, (), (1984) · Zbl 0522.68027
[10] Fortune, S.; Leivant, D.; O’Donnell, M., The expressiveness of simple and second order type structures, J. assoc. comput. Mach., 30, (1983) · Zbl 0519.68046
[11] Ganzinger, H., Parameterized specifications: parameter passing and optimizing implementation, ()
[12] Lambeck, J.; Scott, P., Introduction to higher order categorical logic, (1986), Cambridge Univ. Press New York · Zbl 0596.03002
[13] Levy, J.-J., An algebraic interpretation of the λ-β-κ-calculus and an application of a labeled lambda calculus, Theoret. comput. sci., 2, (1976)
[14] Lipeck, U., Ein algebraischer kalkuel fuer einen strukturierten entwurf von datenabstraktionen, (), Ber. Nr. 148 · Zbl 0506.68023
[15] Pair, C., Abstract data types and algebraic semantics of programming languages, Theoret. comput sci., 18, (1982) · Zbl 0499.68010
[16] Poigné, A., Another look at parameterization using algebraic specifications with subsorts, () · Zbl 0584.68042
[17] Poigné, A., On specifications, theories and models with higher types, Inform. and control, 68, 1-46, (1986) · Zbl 0591.68019
[18] Poigné, A.; Voss, J., Programs over algebraic specifications—on the implementation of abstract data types, (1983), Abt. Informatik, Universität Dortmund, Ber. Nr. 171
[19] Poigné, A.; Voss, J., On the implementation of abstract data types by programming language constructs, () · Zbl 0563.68016
[20] Pottinger, G., The church-rosser theorem for the typed λ-calculus with extensional pairing, (1979), Carnegie-Mellon University Pittsburgh, preprint
[21] Stenlund, S., Combinators, lambda terms, and proof theory, (1972), Reidel Dordrecht · Zbl 0248.02032
[22] Tait, W.W., Intensional interpretation of functionals of finite type, J. symbolic logic, 32, (1967) · Zbl 0174.01202
[23] Voss, J., Programme über algebraischen spezifikationen—zur implementierung von abstrakten datentypen, diplomarbeit, (1983), Abt. Informatik, Universität Dortmund
[24] Sannella, D.T.; Wirsing, M., A kernel language for algebraic specification and implementation, () · Zbl 0517.68043
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.