Abstract
The aim of this paper is to show that the concept of dependent type is necessary and appropriate for a specification language. This is examplified by expressing the type SPEC of all specifications, two different approaches to parameterization, and (a simple variant of) Weber's and Ehrig's module specifications. In particular the formalization of the parameterization concepts gives the solution to the open problem, how to combine the theory of institutions with the lambda calculus approach to parameterization.
This work has been partially sponsored by Forwiss (Bayer. Forschungszentrum für Wissensbasierte Systeme), the ESPRIT-working group COMPASS and the DFG-project SPECTRUM.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Burstall, J. Goguen Putting theories together to make specifications. Proc. 5th Internat. Joint Conf. on Artificial Intelligence, Cambridge Mass., pp. 1045–1058, 1977.
R. Burstall, J. Goguen The semantics of CLEAR, a specification language. In: D. Bjorner (ed.): Proc. Advanced Course on Abstract Software Specifications. Lecture Notes in Computer Science. 86, Springer, Berlin, pp. 292–323, 1980.
M. Breu, M. Broy, T. Grünler, F. Nickl PAnndA-S Semantics Passau, 1989.
Th. Coquand, G. Huet The Calculus of Constructions. Information and Computation 76, pp. 95–120, 1988.
R. Dyckhoff Category Theory as an extension of Martin-Löf Type Theory. Department of Computational Science, University of St. Andrews, Techn. Report CS/85/3, 1985.
H.-D. Ehrich On the theory of specification, implementation and parameterization of abstract data types. J. ACM 29(1), pp. 206–277, 1982.
H. Ehrig, H.-J. Kreowski, J. Thatcher, E. Wagner, J. Wright Parameterized data types in algebraic specification languages (short version). In: J. de Bakker, J. van Leuwen (eds.): Proc. 7th Internat. Coll. on Automata, Languages and Programming. Lecture Notes in Computer Science 85, Springer, Berlin, pp. 157–168, 1980.
H. Ehrig, B. Mahr Fundamentals of Algebraic Specifications I. EATCS Monographs on Theoretical Computer Science 6, Springer, Berlin, 1985.
K. Futatsugi, J. Goguen, J.-P. Jouannaud, J. Meseguer Principles of OBJ-2. Proc. POPL 1985, pp. 52–66, 1985.
J. Goguen, R. Burstall Introducing Institutions. Proc. Logics of Programming Workshop, Carnegie-Mellon, Lecture Notes in Computer Science 164, Springer, Berlin, pp. 221–256, 1984.
J. Guttag, J. Horning, J. Wing Larch in Five Easy Pieces. Digital, Systems Research Center, Palo Alto, California, 1985.
P. Martin-Löf Intuitionistic Type Theory. Bibliopolis, Naples, 1984.
D. MacQueen Using Dependent Types to Express Modular Structure. In Proc. 13-th ACM Symp. on Principles of Programming Languages, pp. 277–286, 1986.
D. Sannella, A. Tarlecki Specifications in Arbitrary Institutions. Information and Computation 76, pp. 165–210, 1988.
D. Sannella, S. Sokolowski, A. Tarlecki Toward formal development of programs from algebraic specifications: parameterisation revisited. Draft, 1990.
D. Sannella, M. Wirsing A kernel language for algebraic specification and implementation. In: M. Karpinsky (ed.): Coll. on Foundations of Computation Theory, Lecture Notes in Computer Science 158, Springer, Berlin, pp. 413–427, 1983.
R. Burstall, J. Goguen, A. Tarlecki Some Fundamental Algebraic Tools for the Semantics of Computation. Part III: Indexed Categories. ECS-LFCS-88-60, Techn. Report, Univ. Edinburgh, 1988.
J. Thatcher, E. Wagner, J. Wright Data type specification: Parameterization and the power of specification techniques. TOPLAS 4, pp. 711–773, 1982.
H. Weber, H. Ehrig Programming in the large with algebraic module specifications. H.J. Kugler (ed.): Proc. IFIP, 10th World Computer Congress. North Holland, Amsterdam, pp. 675–684, 1986.
M. Wirsing Algebraic Specifications. In Handbook of Theoretical Computer Science Volume B, Formal Models and Semantics ed. J. van Leeuwen, Elsevier, Amsterdam, pp.675–788, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Streicher, T., Wirsing, M. (1991). Dependent types considered necessary for specification languages. In: Ehrig, H., Jantke, K.P., Orejas, F., Reichel, H. (eds) Recent Trends in Data Type Specification. ADT 1990. Lecture Notes in Computer Science, vol 534. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54496-8_17
Download citation
DOI: https://doi.org/10.1007/3-540-54496-8_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54496-8
Online ISBN: 978-3-540-38416-8
eBook Packages: Springer Book Archive