{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:56Z","timestamp":1749124076881},"reference-count":59,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5663,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,9]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129500000256","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:02:15Z","timestamp":1236157335000},"page":"333-363","source":"Crossref","is-referenced-by-count":15,"title":["Program specification and data refinement in type theory"],"prefix":"10.1017","volume":"3","author":[{"given":"Zhaohui","family":"Luo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000256_ref028","unstructured":"Luo Z. (1990a) An Extended Calculus of Constructions, PhD thesis, University of Edinburgh. Also as Report CST-65\u201390\/ECS-LFCS-90\u2013118, Department of Computer Science, University of Edinburgh."},{"key":"S0960129500000256_ref008","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129500000256_ref048","unstructured":"Pollack R. (1990) Implicit syntax. In: The Preliminary Proceedings of the 1st Workshop on Logical Frameworks."},{"key":"S0960129500000256_ref045","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90031-A"},{"key":"S0960129500000256_ref027","volume-title":"Proc. of the Fourth Ann. Symp. On Logic in Computer Science","author":"Luo","year":"1989"},{"key":"S0960129500000256_ref024","unstructured":"Huet G. (1987) A calculus with type:type. (Unpublished manuscript)"},{"key":"S0960129500000256_ref042","unstructured":"Milner R. , Tofte M. and Harper R. (1990) The Definition of Standard ML, MIT."},{"key":"S0960129500000256_ref036","unstructured":"MacQueen D. (1981) Structures and parameterization in a typed functional language. Proc. Symp.on Functional Programming and Computer Architecture."},{"key":"S0960129500000256_ref003","volume-title":"An approach to program specification and development in constructions","author":"Burstall","year":"1989"},{"key":"S0960129500000256_ref056","doi-asserted-by":"crossref","unstructured":"Sannella D. and Wirsing M. (1983) A kernal language for algebraic specification and implementation. Technical Report CSR-155\u201383, Dept of Computer Science, University of Edinburgh.","DOI":"10.1007\/3-540-12689-9_122"},{"key":"S0960129500000256_ref013","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"de Bruijn","year":"1980"},{"key":"S0960129500000256_ref026","article-title":"Specification techniques for data abstraction","volume":"1","author":"Liskov","year":"1975","journal-title":"IEEE Trans. On Software Engineering"},{"key":"S0960129500000256_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S0960129500000256_ref034","volume-title":"LEGO Proof Development System: User's Manual","author":"Luo","year":"1992"},{"key":"S0960129500000256_ref007","volume-title":"Deliverables: a categorical approach to program development in type theory","author":"Burstall","year":"1992"},{"key":"S0960129500000256_ref037","doi-asserted-by":"crossref","unstructured":"MacQueen D. (1986) Using dependent types to express modular structure. Proc. 13th Principles of Programming Languages.","DOI":"10.1145\/512644.512670"},{"key":"S0960129500000256_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7"},{"key":"S0960129500000256_ref017","article-title":"Principles of OBJ2","volume":"85","author":"Futatsugi","year":"1985","journal-title":"Proc. POPL"},{"key":"S0960129500000256_ref014","unstructured":"Ehrig H. , Fey W. and Hansen H. (1983) ACT ONE: an algebraic specification language with two levels of semantics. Technical Report 83\u201303, Technical University of Berlin, Fachbereich Informatik."},{"key":"S0960129500000256_ref059","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50939-9_124"},{"key":"S0960129500000256_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129500000256_ref032","volume-title":"Springer- Verlag Lecture Notes in Computer Science","author":"Luo","year":"1992"},{"key":"S0960129500000256_ref025","volume-title":"Systematic Software Development using VDM","author":"Jones","year":"1986"},{"key":"S0960129500000256_ref019","volume-title":"Current Trends in Programming Methodology, Vol. 4","author":"Goguen","year":"1978"},{"key":"S0960129500000256_ref006","volume-title":"Deliverables: an approach to program development in the calculus of constructions","author":"Burstall","year":"1991"},{"key":"S0960129500000256_ref051","unstructured":"Sannella D. , Sokolowski S. and Tarlecki A. (1990) Toward formal development of programs from algebraic specifications: Parameterization revisited. (Draft)"},{"key":"S0960129500000256_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0960129500000256_ref030","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90062-7"},{"key":"S0960129500000256_ref021","article-title":"Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions","volume":"89","author":"Harper","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"S0960129500000256_ref038","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f P. (1975) An intuitionistic theory of types: predicative part. In: Rose H. and Shepherdson J. C. (eds.) Logic Colloquium'73.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S0960129500000256_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887198"},{"key":"S0960129500000256_ref029","volume-title":"A problem of adequacy: conservativity of calculus of constructions over higher-order logic","author":"Luo","year":"1990"},{"key":"S0960129500000256_ref009","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable","year":"1986"},{"key":"S0960129500000256_ref039","volume-title":"Logic, Methodology and Philosophy of Science VI","author":"Martin-L\u00f6f","year":"1982"},{"key":"S0960129500000256_ref031","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"Luo","year":"1991"},{"key":"S0960129500000256_ref049","unstructured":"Reus B. and Streicher T. (1992) Lifting the laws of module algebra to deliverables. Technical report, Ludwig-Maximilians-Universit\u00e4t M\u00fcnichen, Institut f\u00fcr Informatik."},{"key":"S0960129500000256_ref018","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, PhD thesis, Universit\u00e9 Paris VII."},{"key":"S0960129500000256_ref055","doi-asserted-by":"publisher","DOI":"10.1007\/BF00283329"},{"key":"S0960129500000256_ref023","volume-title":"To H. B. Curry: Essays on Combinatory Logic","author":"Howard","year":"1980"},{"key":"S0960129500000256_ref047","unstructured":"Pollack R. (1989) The theory of LEGO. (Manuscript)"},{"key":"S0960129500000256_ref044","volume-title":"Programming in Martin-L\u00f6fs Type Theory: an introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0960129500000256_ref035","volume-title":"How to Use LEGO: a preliminary user's manual","author":"Luo","year":"1989"},{"key":"S0960129500000256_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61284-8"},{"key":"S0960129500000256_ref040","unstructured":"Martin-L\u00f6f P. (1984) Intuitionistic Type Theory, Bibliopolis."},{"key":"S0960129500000256_ref050","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0960129500000256_ref046","unstructured":"Paulin-Mohring C. (1989) Extracting F\u03c9 programs from proofs in the calculus of constructions. Proc. POPL 89."},{"key":"S0960129500000256_ref041","doi-asserted-by":"crossref","unstructured":"McKinna J. (1992) Deliverables: a categorical approach to program development in type theory, PhD thesis, Department of Computer Science, University of Edinburgh.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"S0960129500000256_ref054","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90008-9"},{"key":"S0960129500000256_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"S0960129500000256_ref033","volume-title":"A Theory of Dependent Types and Computer Science","author":"Luo","year":"1993"},{"key":"S0960129500000256_ref058","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90051-4"},{"key":"S0960129500000256_ref057","unstructured":"Wand P. (1992) Functional programming and verification with lego, Master's thesis, Department of Computer Science, University of Edinburgh."},{"key":"S0960129500000256_ref053","first-page":"364\u2013389","article-title":"Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming","volume":"240","author":"Sannella","year":"1987","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129500000256_ref012","volume-title":"Combinatory Logic","volume":"1","author":"Curry","year":"1958"},{"key":"S0960129500000256_ref020","article-title":"Abstract data types and software validation","volume":"21","author":"Guttag","year":"1976","journal-title":"Comm. ACM"},{"key":"S0960129500000256_ref052","volume-title":"Toward formal development of programs from algebraic specifications: Parameterization revisited","author":"Sannella","year":"1992"},{"key":"S0960129500000256_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_1"},{"key":"S0960129500000256_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_41"},{"key":"S0960129500000256_ref043","unstructured":"Nordstr\u00f6m B. and Petersson K. (1983) Types and specifications. Proceedings of IFIP'83 915\u2013920."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T21:43:25Z","timestamp":1557956605000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000256\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":59,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["S0960129500000256"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000256","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}