{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:05:13Z","timestamp":1725663913390},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578673"},{"type":"electronic","value":"9783540483618"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57867-6_16","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:32:40Z","timestamp":1330263160000},"page":"268-279","source":"Crossref","is-referenced-by-count":1,"title":["A semantic basis for logic-independent transformation"],"prefix":"10.1007","author":[{"given":"Junbo","family":"Liu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"16_CR1","volume-title":"Arrows, Structures, and Functors-the Categorical Imperative","author":"M. Arbib","year":"1975","unstructured":"M. Arbib, E. Manes. Arrows, Structures, and Functors-the Categorical Imperative. New York, London: Academic Press 1975."},{"key":"16_CR2","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"H. Ehrig","year":"1985","unstructured":"H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science New York: Springer (1985)."},{"key":"16_CR3","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"H. Ehrig","year":"1990","unstructured":"H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification II. EATCS Monographs on Theoretical Computer Science New York: Springer (1990)."},{"key":"16_CR4","unstructured":"P. Gardner. Representing Logics in Type Theory. Phd Thesis, LFCS Report ECS-LFCS-92-227, Dept. of Computer Science, Uni. of Edinburgh."},{"issue":"No.1","key":"16_CR5","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. A. Goguen","year":"1992","unstructured":"J.A. Goguen, R.M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, vol. 39, No. 1, pp 95\u2013146 (Jan. 1992).","journal-title":"J. ACM"},{"key":"16_CR6","unstructured":"R. Harper, F. Honsell, G. Plotkin. A Framework for Defining Logics. Proc. 2nd IEEE Symp. on Logic in Computer Science, Conell, pp 194\u2013204 (1987)."},{"key":"16_CR7","unstructured":"R. Harper, D. Sannella, A. Tarlecki. Structure and Representation in LF. LFCS Report ECS-LFCS-89-75, Dept. of Computer Science, Uni. of Edinburgh."},{"key":"16_CR8","first-page":"250","volume":"389","author":"R. Harper","year":"1989","unstructured":"R. Harper, D. Sannella, A. Tarlecki. Logic Representation in LF. Proc. 3nd Summer Conference in Category Theory and Computer Science, LNCS 389, pp 250\u2013272 (1989).","journal-title":"LNCS"},{"key":"16_CR9","unstructured":"B. Krieg-Br\u00fcckner, D. Sannella. Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. Proc. TAPSOFT 91, LNCS 582(1991)."},{"key":"16_CR10","unstructured":"B. Krieg-Br\u00fcckner, E. Karlsen, J. Liu, O. Traynor. The PROSPECTRA Methodology and System: Uniform Transformational (Meta-) Development. VDM '91: Formal Software Development Methods, S. Prchn W.J. Toctenel (eds.), LNCS 552, pp 362\u2013397."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"B. Hoffmann, B. Krieg-Br\u00fcckner (eds.): PROgram development by SPECification and TRAnsformation: Methodology, Language Family, System. LNCS 680 (1993).","DOI":"10.1007\/3-540-56733-X"},{"key":"16_CR12","unstructured":"J. Lambek, P.J. Scott. Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press 1986."},{"key":"16_CR13","unstructured":"Z. Luo. An Extended Calculus of Constructions. Phd Thesis, LFCS Report ECS-LFCS-90-118, Dept. of Computer Science, Uni. of Edinburgh."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"J. Meseguer. General Logics, Proc. of the Logic Colloquium '87, H. D. Ebbinghaus et al. (eds.), North Holland.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin (eds.): Logical Frameworks. Cambridge University Press 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"16_CR16","unstructured":"D. Sannella, S. Sokolowski, A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterization revisited. Report 6\/90, Informatik, Universit\u00e4t Bremen (1990)."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"D. Sannella, A. Tarlecki. Towards formal development of programs from algebraic specifications: implementations revisited. In H. Ehrig et al.(eds.): TAPSOFT 87 LNCS 249 pp 96\u2013110 (1987).","DOI":"10.1007\/3-540-17660-8_50"},{"key":"16_CR18","first-page":"413","volume":"158","author":"D. Sannella","year":"1983","unstructured":"D. Sannella, M. Wirsing. A kernel language for algebraic specifications and implementations LNCS 158, pp 413\u2013427 (1983).","journal-title":"LNCS"},{"key":"16_CR19","unstructured":"L. Paulson. The foundations of a generic theorem prover. Technical Report 130, Computer Laboratory, University of Cambridge."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"L. Paulson. Logics and Computation: interactive proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2, Cambridge University Press 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"16_CR21","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 language. TCS 42, pp 123\u2013249 (1986).","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Data Type Specification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57867-6_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:09:08Z","timestamp":1619572148000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57867-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578673","9783540483618"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-57867-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}