Abstract
This paper presents a comparison between algebraic specifications-in-the-large and a type theoretical formulation of modular specifications, called deliverables. It is shown that the laws of module algebra can be translated to laws about deliverables which can be proved correct in type theory. The adequacy of the Extended Calculus of Constructions as a possible implementation of type theory is discussed and it is explained how the reformulation of the laws is influenced by this choice.
This work was partially sponsored by the BMFT-project KORSO
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J. A. Bergstra, J. Heering, P. Klint: Algebraic Specification. ACM Press, New York, 1989.
R.M. Burstall, J.A. Goguen: The semantics of Clear, a specification language. In: Proc. Advanced Course on Abstract Software Specification. LNCS 86, Springer, Berlin, 1980.
R.M. Burstall, J. McKinna: Deliverables: a categorical approach to program development in type theory. ECS-LFCS-92-242, Dept. of Computer Science, Edinburgh University, 1992.
J. McKinna: Deliverables: a categorical approach to program development in type theory. Ph.D. Thesis, University of Edinburgh, 1992. Also appeared as ECS-LFCS-92-247, Dept. of Computer Science, Edinburgh University, 1992.
J. Leszczylowski, M. Wirsing: Polymorphism, Parameterisation and Typing: An Algebraic Specification Perspective. In: Proc. of the 8th STACS, LNCS 480, Springer, Berlin, p. 1–15.
Z. Luo: ECC, an Extended Calculus of Constructions. In: Proc. of the Fourth Ann. Symp. on Logic in Computer Science (LICS), IEEE, 1989, p. 385–395.
Z. Luo: Program specification and data refinement in type theory. In: Proc. of the Fourth Intern. Conf. on the Theory and Practice of Software Development (TAPSOFT), LNCS 493, Springer, Berlin, 1991, p. 143–168.
Z. Luo: private communication.
Z. Luo, R. Pollack: LEGO Proof Development System: Users' Manual. ECS-LFCS-92-211, Dept. of Computer Science, Edinburgh University, 1992.
B. Norström, K. Petersson, J.M. Smith: Programming in Martin Löf's Type Theory. Oxford University Press, Oxford, 1990.
T. Streicher: Semantics of Type Theory — Correctness, Completeness and Independence Results. Birkhäuser, Boston, 1991.
T. Streicher, M. Wirsing: Dependent types considered necessary for algebraic specification languages. In: Recent Trends in Data Type Specification, Proc. 7th International Workshop on Specification of Abstract Data Types. LNCS 534, Springer, Berlin, 1990, p. 323–340.
M. Wirsing: Structured algebraic specifications: a kernel language. Theoretical Computer Science 42, 1986, p. 123–249.
M. Wirsing: Algebraic Specification in J.V. Leeuwen (ed.): Handbook of Theoretical Computer Science, Volume B, Elsevier, Amsterdam, 1990, p. 675–788.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reus, B., Streicher, T. (1993). Verifying properties of module construction in type theory. In: Borzyszkowski, A.M., Sokołowski, S. (eds) Mathematical Foundations of Computer Science 1993. MFCS 1993. Lecture Notes in Computer Science, vol 711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57182-5_57
Download citation
DOI: https://doi.org/10.1007/3-540-57182-5_57
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57182-7
Online ISBN: 978-3-540-47927-7
eBook Packages: Springer Book Archive