Hostname: page-component-77c89778f8-5wvtr Total loading time: 0 Render date: 2024-07-21T12:12:44.389Z Has data issue: false hasContentIssue false
  • English
  • Français

Program specification and data refinement in type theory†

Published online by Cambridge University Press:  04 March 2009

Zhaohui Luo
Zhaohui Luo
Affiliation:
Department of Computer Science, University of Edinburgh, Mayfield Road, Edinburgh EH9 3JZ
Get access Rights & Permissions [Opens in a new window]

Abstract

The study of type theory may offer a uniform language for modular programming, structured specification and logical reasoning. We develop an approach to program specification and data refinement in a type theory with a strong logical power and nice structural mechanisms to show that it provides an adequate formalism for modular development of programs and specifications. Specification of abstract data types is considered, and a notion of abstract implementation between specifications is defined in the type theory and studied as a basis for correct and modular development of programs by stepwise refinement. The higher-order structural mechanisms in the type theory provide useful and flexible tools (specification operations and parameterized specifications) for modular design and structured specification. Refinement maps (programs and design decisions) and proofs of implementation correctness can be developed by means of the existing proof development systems based on type theories.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 3 , Issue 3 , September 1993 , pp. 333 - 363
Copyright
Copyright © Cambridge University Press 1993

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Backhouse, R., Chisholm, P., AND Malcolm, G. (1989) Do-it-youself type theory. Formal Aspects of Computing 1 (1).CrossRefGoogle Scholar
Böhm, C. and Berarducci, A. (1985) Automatic synthesis of typed λ-programs on term algebras.Theoretical Computer Science 39.CrossRefGoogle Scholar
Burstall, R. (1989) An approach to program specification and development in constructions. Talk given in Workshop on Programming Logic, Bastad, Sweden.Google Scholar
Burstall, R. and Goguen, J. (1980) The semantics of Clear, a specification language. Springer-Verlag Lecture Notes in Computer Science 86.CrossRefGoogle Scholar
Burstall, R. and Lampson, B. (1984) Pebble, a kernel language for modules and abstract data types.Springer-Verlag Lecture Notes in Computer Science 173.CrossRefGoogle Scholar
Burstall, R. and McKinna, J. (1991) Deliverables: an approach to program development in the calculus of constructions. LFCS report ECS-LFCS-91–133, Dept of Computer Science, University of Edinburgh.Google Scholar
Burstall, R. and McKinna, J. (1992) Deliverables: a categorical approach to program development in type theory. LFCS report ECS-LFCS-92–242, Dept of Computer Science, University of Edinburgh.Google Scholar
Church, A. (1940) A formulation of the simple theory of types. J. Symbolic Logic 5 (1).CrossRefGoogle Scholar
Constable, R.et.al.. (1986) Implementing Mathematics with the NuPRL Proof Development System, Prentice Hall.Google Scholar
Coquand, T. and Huet, G. (1988) The calculus of constructions. Information and Computation 76 (2/3).CrossRefGoogle Scholar
Coquand, T. and Paulin-Mohring, C. (1990) Inductively defined types. Springer-Verlag Lecture Notes in Computer Science 417.CrossRefGoogle Scholar
Curry, H. and Feys, R. (1958) Combinatory Logic, volume 1, North-Holland Publishing Company.Google Scholar
de Bruijn, N. (1980) A survey of the project AUTOMATH. In: Hindley, J. and Seldin, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press.Google Scholar
Ehrig, H., Fey, W. and Hansen, H. (1983) ACT ONE: an algebraic specification language with two levels of semantics. Technical Report 83–03, Technical University of Berlin, Fachbereich Informatik.Google Scholar
Ehrig, H. and Mahr, B. (1985) Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, Springer.CrossRefGoogle Scholar
Ehrig, H. and Mahr, B. (1990) Fundamentals of Algebraic Specification 2: Module specifications and Constraints, Springer.CrossRefGoogle Scholar
Futatsugi, K., Goguen, J., Jouannaud, J.-P. and Meseguer, J. (1985) Principles of OBJ2. Proc. POPL 85.Google Scholar
Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, PhD thesis, Université Paris VII.Google Scholar
Goguen, J., Thatcher, J. and Wagner, E. (1978) Abstract data types as initial algebras and the correctness of data representation. In: Yeh, R., (ed.) Current Trends in Programming Methodology, Vol. 4, Prentice Hall.Google Scholar
Guttag, J., Horowitz, E. and Musser, D. (1976) Abstract data types and software validation. Comm. ACM 21 (12).Google Scholar
Harper, R. and Pollack, R. (1991) Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions. Theoretical Computer Science 89 (1).Google Scholar
Hoare, C. (1972) Proofs of correctness of data representation. Acta Informatica. 1 (1).CrossRefGoogle Scholar
Howard, W. A. (1980) The formulae-as-types notion of construction. In: Hindley, J. and Seldin, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Academic Press.Google Scholar
Huet, G. (1987) A calculus with type:type. (Unpublished manuscript)Google Scholar
Jones, C. (1986) Systematic Software Development using VDM, Prentice Hall.Google Scholar
Liskov, B. and Zilles, S. (1975) Specification techniques for data abstraction. IEEE Trans. On Software Engineering SE-1 (1)Google Scholar
Luo, Z. (1989) ECC, an extended calculus of constructions. In: Proc. of the Fourth Ann. Symp. On Logic in Computer Science, Asilomar, California, U.S.A.Google Scholar
Luo, Z. (1990a) An Extended Calculus of Constructions, PhD thesis, University of Edinburgh. Also as Report CST-65–90/ECS-LFCS-90–118, Department of Computer Science, University of Edinburgh.Google Scholar
Luo, Z. (1990b) A problem of adequacy: conservativity of calculus of constructions over higher-order logic. Technical report, LFCS report series ECS-LFCS-90–121, Department of Computer Science, University of Edinburgh.Google Scholar
Luo, Z. (1991a) A higher-order calculus and theory abstraction. Information and Computation 90 (1) 107–137.CrossRefGoogle Scholar
Luo, Z. (1991b) Program specification and data refinement in type theory. Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT). Springer-Verlag Lecture Notes in Computer Science 493. Also as LFCS report ECS-LFCS-91–131, Dept. of Computer Science, Edinburgh University.Google Scholar
Luo, Z. (1992) A unifying theory of dependent types: the schematic approach. Proc. of Symp. On Logical Foundations of Computer Science (Logic at Tver'92). Springer- Verlag Lecture Notes in Computer Science 620. Also as LFCS Report ECS-LFCS-92–202, Dept. of Computer Science, University of Edinburgh.Google Scholar
Luo, Z. (1993) A Theory of Dependent Types and Computer Science, The Oxford University Press. (To appear)Google Scholar
Luo, Z. and Pollack, R. (1992) LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92–211, Department of Computer Science, University of Edinburgh.Google Scholar
Luo, Z., Pollack, R. and Taylor, P. (1989) How to Use LEGO: a preliminary user's manual. LFCS Technical Notes LFCS-TN-27, Dept. of Computer Science, Edinburgh University.Google Scholar
MacQueen, D. (1981) Structures and parameterization in a typed functional language. Proc. Symp.on Functional Programming and Computer Architecture.Google Scholar
MacQueen, D. (1986) Using dependent types to express modular structure. Proc. 13th Principles of Programming Languages.CrossRefGoogle Scholar
Martin-Löf, P. (1975) An intuitionistic theory of types: predicative part. In: Rose, H. and Shepherdson, J. C. (eds.) Logic Colloquium'73.CrossRefGoogle Scholar
Martin-Löf, P. (1982) Constructive mathematics and computer programming. In: Cohen, L.C.et.al. (eds.) Logic, Methodology and Philosophy of Science VI, Amsterdam, North-Holland.Google Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory, Bibliopolis.Google Scholar
McKinna, J. (1992) Deliverables: a categorical approach to program development in type theory, PhD thesis, Department of Computer Science, University of Edinburgh.CrossRefGoogle Scholar
Milner, R., Tofte, M. and Harper, R. (1990) The Definition of Standard ML, MIT.Google Scholar
Nordström, B. and Petersson, K. (1983) Types and specifications. Proceedings of IFIP'83 915–920.Google Scholar
Nordström, B., Petersson, K. and Smith, J. (1990) Programming in Martin-Löfs Type Theory: an introduction, Oxford University Press.Google Scholar
Ore, C.-E. (1992) The Extended Calculus of Constructions (ECC) with inductive types. Information and Computation 99 (2) 231–264.CrossRefGoogle Scholar
Paulin-Mohring, C. (1989) Extracting Fω programs from proofs in the calculus of constructions. Proc. POPL 89.Google Scholar
Pollack, R. (1989) The theory of LEGO. (Manuscript)Google Scholar
Pollack, R. (1990) Implicit syntax. In: The Preliminary Proceedings of the 1st Workshop on Logical Frameworks.Google Scholar
Reus, B. and Streicher, T. (1992) Lifting the laws of module algebra to deliverables. Technical report, Ludwig-Maximilians-Universität Münichen, Institut für Informatik.Google Scholar
Reynolds, J. (1974) Towards a theory of type structure. Springer-Verlag Lecture Notes in Computer Science 19.CrossRefGoogle Scholar
Sannella, D., Sokolowski, S. and Tarlecki, A. (1990) Toward formal development of programs from algebraic specifications: Parameterization revisited. (Draft)Google Scholar
Sannella, D., Sokolowski, S. and Tarlecki, A. (1992) Toward formal development of programs from algebraic specifications: Parameterization revisited. LFCS Report ECS-LFCS-92–222, Department of Computer Science, University of Edinburgh.Google Scholar
Sannella, D. and Tarlecki, A. (1987) Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming. Springer-Verlag Lecture Notes in Computer Science 240 364–389.Google Scholar
Sannella, D. and Tarlecki, A. (1988a) Specifications in arbitrary institutions. Information and Computation 76.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (1988b) Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica 25.CrossRefGoogle Scholar
Sannella, D. and Wirsing, M. (1983) A kernal language for algebraic specification and implementation. Technical Report CSR-155–83, Dept of Computer Science, University of Edinburgh.CrossRefGoogle Scholar
Wand, P. (1992) Functional programming and verification with lego, Master's thesis, Department of Computer Science, University of Edinburgh.Google Scholar
Wirsing, M. (1986) Structured algebraic specifications: a kernel language. Theoretical Computer Science 42 123–249.CrossRefGoogle Scholar
Wirsing, M. and Broy, M. (1989) A modular framework for specification and implementation. TAPSOFT'89. Springer-Verlag Lecture Notes in Computer Science 351.CrossRefGoogle Scholar