Dependent types considered necessary for specification languages | SpringerLink
Skip to main content
Springer Nature Link
Log in

Dependent types considered necessary for specification languages

  • Conference paper
  • First Online:
Recent Trends in Data Type Specification (ADT 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 534))

Included in the following conference series:

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.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. R. Burstall, J. Goguen Putting theories together to make specifications. Proc. 5th Internat. Joint Conf. on Artificial Intelligence, Cambridge Mass., pp. 1045–1058, 1977.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. M. Breu, M. Broy, T. Grünler, F. Nickl PAnndA-S Semantics Passau, 1989.

    Google Scholar 

  4. Th. Coquand, G. Huet The Calculus of Constructions. Information and Computation 76, pp. 95–120, 1988.

    Article  Google Scholar 

  5. 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.

    Google Scholar 

  6. H.-D. Ehrich On the theory of specification, implementation and parameterization of abstract data types. J. ACM 29(1), pp. 206–277, 1982.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. H. Ehrig, B. Mahr Fundamentals of Algebraic Specifications I. EATCS Monographs on Theoretical Computer Science 6, Springer, Berlin, 1985.

    Google Scholar 

  9. K. Futatsugi, J. Goguen, J.-P. Jouannaud, J. Meseguer Principles of OBJ-2. Proc. POPL 1985, pp. 52–66, 1985.

    Google Scholar 

  10. 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.

    Google Scholar 

  11. J. Guttag, J. Horning, J. Wing Larch in Five Easy Pieces. Digital, Systems Research Center, Palo Alto, California, 1985.

    Google Scholar 

  12. P. Martin-Löf Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

    Google Scholar 

  13. D. MacQueen Using Dependent Types to Express Modular Structure. In Proc. 13-th ACM Symp. on Principles of Programming Languages, pp. 277–286, 1986.

    Google Scholar 

  14. D. Sannella, A. Tarlecki Specifications in Arbitrary Institutions. Information and Computation 76, pp. 165–210, 1988.

    Article  Google Scholar 

  15. D. Sannella, S. Sokolowski, A. Tarlecki Toward formal development of programs from algebraic specifications: parameterisation revisited. Draft, 1990.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. J. Thatcher, E. Wagner, J. Wright Data type specification: Parameterization and the power of specification techniques. TOPLAS 4, pp. 711–773, 1982.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, D-8940, Passau, FRG

    T. Streicher & M. Wirsing

Authors
  1. T. Streicher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

H. Ehrig K. P. Jantke F. Orejas H. Reichel

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation