{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:53:14Z","timestamp":1743054794954,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678984"},{"type":"electronic","value":"9783540446163"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/978-3-540-44616-3_23","type":"book-chapter","created":{"date-parts":[[2010,10,14]],"date-time":"2010-10-14T14:09:44Z","timestamp":1287065384000},"page":"401-418","source":"Crossref","is-referenced-by-count":9,"title":["Higher-Order Logic and Theorem Proving for Structured Specifications"],"prefix":"10.1007","author":[{"given":"Tomasz","family":"Borzyszkowski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, INC., London (1986)"},{"key":"23_CR2","series-title":"Studies in Logic and The Foundations of Mathematics","volume-title":"The Lambda Calculus Its Syntax and Semantics","author":"H.P. Barendregt","year":"1998","unstructured":"Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics. Studies in Logic and The Foundations of Mathematics. Elsevier, Amsterdam (1998)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-48483-3_2","volume-title":"Recent Trends in Algebraic Development Techniques","author":"T. Borzyszkowski","year":"1998","unstructured":"Borzyszkowski, T.: Moving specification structures between logical systems. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol.\u00a01589, pp. 16\u201328. Springer, Heidelberg (1998)"},{"unstructured":"Borzyszkowski, T.: Logical systems for structured specifications. Special issue of Theoretical Computer Science (to appear), See \n                      http:\/\/monika.univ.gda.pl\/~mattb\/papers.html","key":"23_CR4"},{"unstructured":"CASL The Common Algebraic Specification Language - Summary, by The CoFI Task Group on Language Design. Version 1.0 (March 19, 1999), Document is available on \n                      http:\/\/www.brics.dk\/Projects\/CoFI\/Notes\/S-9\/\n                     and \n                      ftp:\/\/ftp.brics.dk\/Projects\/CoFI\/Notes\/S-9\/","key":"23_CR5"},{"key":"23_CR6","series-title":"Undergraduate Texts in Mathematics","volume-title":"Mathematical Logic","author":"H.-D. Ebbinghaus","year":"1996","unstructured":"Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Undergraduate Texts in Mathematics. Springer, Heidelberg (1996)","edition":"2"},{"key":"23_CR7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specifications and programming. Journal of the Assoc. for Computing Machinery\u00a039, 95\u2013146 (1992)","journal-title":"Journal of the Assoc. for Computing Machinery"},{"key":"23_CR8","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"23_CR9","first-page":"279","volume-title":"Logic Colloquium 1987","author":"J. Meseguer","year":"1989","unstructured":"Meseguer, J.: General logic. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium 1987, pp. 279\u2013329. North-Holland, Amsterdam (1989)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Recent Trends in Algebraic Development Techniques","author":"T. Mossakowski","year":"1998","unstructured":"Mossakowski, T., Kolyang, Krieg-Br\u00fcckner, B.: Static Semantic Analysis and Theorem Proving for CASL. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, Springer, Heidelberg (1998)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle: A Generic Theorem Prover","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"23_CR12","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/BF01191893","volume":"29","author":"D. Sannella","year":"1992","unstructured":"Sannella, D., SokoGlowski, S., Tarlecki, A.: Towards formal development of programs from algebraic specification: parameterization revisited. Acta Informatica\u00a029, 689\u2013736 (1992)","journal-title":"Acta Informatica"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/3-540-61629-2_59","volume-title":"Recent Trends in Data Type Specification","author":"A. Tarlecki","year":"1996","unstructured":"Tarlecki, A.: Moving between logical systems. Recent Trends in Data Type Specifications. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol.\u00a01130, pp. 478\u2013502. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-44616-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:41:00Z","timestamp":1676691660000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-44616-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678984","9783540446163"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-44616-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}