{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083828},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540539827"},{"type":"electronic","value":"9783540465638"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-53982-4_9","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:21:39Z","timestamp":1330208499000},"page":"143-168","source":"Crossref","is-referenced-by-count":10,"title":["Program specification and data refinement in type theory"],"prefix":"10.1007","author":[{"given":"Zhaohui","family":"Luo","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"C. B\u00f6hm and A. Beradurcci. Automatic synthesis of typed \u03bb-programs on term algebras. Theoretical Computer Science, 39, 1985.","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"R. Backhouse, P. Chisholm, and G. Malcolm. Do-it-youself type theory. Formal Aspects of Computing, 1(1), 1989.","DOI":"10.1007\/BF01887198"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"M.J. Beeson. Problematic principles in constructive mathematics. Logic Colloquiun'80, 1982.","DOI":"10.1016\/S0049-237X(09)70502-6"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"R. Burstall and J. Goguen. The semantics of Clear, a specification language. Lecture Notes in Computer Science, 86, 1980.","DOI":"10.1007\/3-540-10007-5_41"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"R. Burstall and B. Lampson. Pebble, a kernel language for modules and abstract data types. Lecture Notes in Computer Science, 173, 1984.","DOI":"10.1007\/3-540-13346-1_1"},{"key":"9_CR6","unstructured":"R. Burstall and J. McKinna. Deliverables: an approach to program development in the calculus of constructions. In the preliminary Proceedings of the 1st Workshop on Logical Frameworks, 1990."},{"key":"9_CR7","unstructured":"R.L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2\/3), 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. J. Symbolic Logic, 5(1), 1940.","DOI":"10.2307\/2266170"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Th. Coquand and Ch. Paulin-Mohring. Inductively defined types. Lecture Notes in Computer Science, 417, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9_CR11","unstructured":"N.G. de Bruijn. A survey of the project AUTOMATH. In J. Hindley and J. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980."},{"key":"9_CR12","unstructured":"H. Ehrig, W. Fey, and H. Hansen. ACT ONE: an algebraic specification language with two levels of semantics. Technical Report 83-03, Technical University of Berlin, Fachbereich Informatik, 1983."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Semantics. Springer, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. Proc. POPL 85, 1985.","DOI":"10.1145\/318593.318610"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"J.V. Guttag, E. Horowitz, and D.R. Musser. Abstract data types and software validation. Comm. ACM, 21(12), 1976.","DOI":"10.21236\/ADA029896"},{"key":"9_CR16","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"9_CR17","unstructured":"J.A. Goguen, J.W. Thatcher, and E.G. Wagner. Abstract data types as initial algebras and the correctness of data representation. In R. Yeh, editor, Current Trends in Programming Methodology, Vol. 4. Prentice Hall, 1978."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1(1), 1972.","DOI":"10.1007\/BF00289507"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"R. Harper and R. Pollack. Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions. Theoretical Computer Science, 1989. to appear.","DOI":"10.1007\/3-540-50940-2_39"},{"key":"9_CR20","unstructured":"G. Huet. A calculus with type:type. unpublished manuscript, 1987."},{"key":"9_CR21","unstructured":"C.B. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986."},{"key":"9_CR22","unstructured":"Z. Luo, R. Pollack, and P. Taylor. How to Use LEGO: a preliminary user's manual. LFCS Technical Notes LFCS-TN-27, Dept. of Computer Science, Edinburgh University, 1989."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. ECC, an extended calculus of constructions. In Proc. of the Fourth Ann. Symp. on Logic in Computer Science, Asilomar, California, U.S.A., June 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"9_CR24","unstructured":"Zhaohui Luo. A higher-order calculus and theory abstraction. To appear in Information and Computation, 1989."},{"key":"9_CR25","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90\/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh."},{"key":"9_CR26","unstructured":"Zhaohui Luo. 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, 1990."},{"key":"9_CR27","unstructured":"Zhaohui Luo. A unifying theory of dependent types. manuscript., 1990."},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"B. Liskov and S. Zilles. Specification techniques for data abstraction. IEEE Trans. on Software Engineering, SE-1(1), 1975.","DOI":"10.1109\/TSE.1975.6312816"},{"key":"9_CR29","unstructured":"D.D. MacQueen. Structures and parameterization in a typed functional language. Proc. Symp. on Functional Programming and Computer Architecture, 1981."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: predicative part. Logic Colloquium'73, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"9_CR32","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"9_CR33","unstructured":"T.S.E. Maibaum, M.R. Sadler, and P.A.S. Veloso. Logical implementation, 1983."},{"key":"9_CR34","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT, 1990."},{"key":"9_CR35","unstructured":"B. Nordstr\u00f6m and K. Petersson. Types and specifications. Proceedings of IFIP'83, pages 915\u2013920, 1983."},{"key":"9_CR36","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f's Type Theory: an introduction. Oxford University Press, 1990."},{"key":"9_CR37","unstructured":"C.-H. Ore. The Extended Calculus of Constructions (ECC) with inductive types. draft, 1990."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Ch. Paulin-Mohring. Extracting F \u03c9 programs from proofs in the calculus of constructions. Proc. POPL 89, 1989.","DOI":"10.1145\/75277.75285"},{"key":"9_CR39","unstructured":"R. Pollack. The theory of lego. manuscript, 1989."},{"key":"9_CR40","unstructured":"R. Pollack. Implicit syntax. In the preliminary Proceedings of the 1st Workshop on Logical Frameworks, 1990."},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"J.C. Reynolds. Towards a theory of type structure. Lecture Notes in Computer Science, 19, 1974.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"9_CR42","unstructured":"D. Sannella, S. Sokolowski, and A. Tarlecki. Toward formal development of programs from algebraic specifications: Parameterization revisited. draft, 1990."},{"key":"9_CR43","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-17162-2_133","volume":"240","author":"D. Sannella","year":"1987","unstructured":"D. Sannella and A. Tarlecki. Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming, LNCS 240, pages 364\u2013389, 1987.","journal-title":"Proc. Workshop on Category Theory and Computer Programming, LNCS"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. Specifications in arbitrary institutions. Information and Computation, 76, 1988.","DOI":"10.1016\/0890-5401(88)90008-9"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica, 25, 1988.","DOI":"10.1007\/BF00283329"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"D. Sannella and A. Tarlecki. A kernel specification formalism with higher-order parameterization. Draft, 1990.","DOI":"10.1007\/3-540-54496-8_15"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"D.T. Sannella and M. Wirsing. A kernal language for algebraic specification and implementation. Technical Report CSR-155-83, Dept of Computer Science, University of Edinburgh, 1983.","DOI":"10.1007\/3-540-12689-9_122"},{"key":"9_CR48","unstructured":"P. Taylor and Z. Luo. Theories, mathematical structures and strong sums. manuscript, December 1988."},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"M. Wirsing and M. Broy. A modular framework for specification and implementation. TAPSOFT'89, LNCS, 351, 1989.","DOI":"10.1007\/3-540-50939-9_124"},{"key":"9_CR50","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(86)90051-4","volume":"42","author":"M. Wirsing","year":"1986","unstructured":"M. Wirsing. Structured algebraic specifications: a kernel languages. Theoretical Computer Science, 42:123\u2013249, 1986.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '91"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-53982-4_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:51:54Z","timestamp":1605646314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-53982-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540539827","9783540465638"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/3-540-53982-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}