{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T01:38:29Z","timestamp":1698197909565},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T00:00:00Z","timestamp":1585958400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T00:00:00Z","timestamp":1585958400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s11787-020-00249-y","type":"journal-article","created":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T16:02:26Z","timestamp":1586016146000},"page":"259-277","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Introducing H, an Institution-Based Formal Specification and Verification Language"],"prefix":"10.1007","volume":"14","author":[{"given":"R\u0103zvan","family":"Diaconescu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,4]]},"reference":[{"key":"249_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods for Industrial Applications","year":"1996","unstructured":"Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications \u2013 Specifying and Programming the Steam Boiler Control, volume 1165 of LNCS. Springer, New York (1996)"},{"key":"249_CR2","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1093\/logcom\/11.5.657","volume":"11","author":"C Areces","year":"2001","unstructured":"Areces, C., Blackburn, P., Delany, S.R.: Bringing them all together. J. Log. Comput. 11, 657\u2013669 (2001)","journal-title":"J. Log. Comput."},{"issue":"2","key":"249_CR3","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E Astesiano","year":"2002","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: the common algebraic specification language. Theor. Comput. Sci. 286(2), 153\u2013196 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"249_CR4","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1093\/jigpal\/8.3.339","volume":"8","author":"P Blackburn","year":"2000","unstructured":"Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Log. J. IGPL 8(3), 339\u2013365 (2000)","journal-title":"Log. J. IGPL"},{"issue":"3","key":"249_CR5","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF01049415","volume":"4","author":"P Blackburn","year":"1995","unstructured":"Blackburn, P., Seligman, J.: Hybrid languages. J. Log. Lang. Inf. 4(3), 251\u2013272 (1995)","journal-title":"J. Log. Lang. Inf."},{"key":"249_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-007-0002-4","volume-title":"Hybrid Logic and its Proof-Theory, Volume\u00a037 of Applied Logic Series","author":"T Bra\u00fcner","year":"2011","unstructured":"Bra\u00fcner, T.: Hybrid Logic and its Proof-Theory, Volume\u00a037 of Applied Logic Series. Springer, New York (2011)"},{"key":"249_CR7","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude\u2014A High-Performance Logical Framework. Lecture Notes in Computer Science, vol. 4350. Springer, New York (2007)"},{"key":"249_CR8","unstructured":"Codescu, M.: Hybridisation of institutions in Hets. In: CALCO 2019, 8th Conference on Algebra and Coalgebra in Computer Science (2019)"},{"key":"249_CR9","doi-asserted-by":"crossref","unstructured":"Diaconescu, R.: Extra theory morphisms for institutions: logical semantics for multi-paradigm languages. Appl. Categ. Struct., 6(4), 427\u2013453 (1998). A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997","DOI":"10.1023\/A:1008607717635"},{"key":"249_CR10","doi-asserted-by":"crossref","unstructured":"Diaconescu, R.: Grothendieck institutions. Appl. Categ. Struct., 10(4), 383\u2013402 (2002). Preliminary version appeared as IMAR Preprint 2-2000, ISSN 250-3638, (February 2000)","DOI":"10.1023\/A:1016330812768"},{"key":"249_CR11","volume-title":"Institution-Independent Model Theory","author":"R Diaconescu","year":"2008","unstructured":"Diaconescu, R.: Institution-Independent Model Theory. Birkh\u00e4user, Basel (2008)"},{"issue":"2","key":"249_CR12","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1016\/j.jlap.2009.09.001","volume":"79","author":"R Diaconescu","year":"2010","unstructured":"Diaconescu, R.: Quasi-boolean encodings and conditionals in algebraic specification. J. Log. Algebr. Program. 79(2), 174\u2013188 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"249_CR13","doi-asserted-by":"crossref","unstructured":"Diaconescu, R.: From universal logic to computer science, and back. In:\u00a0Ciobanu, G., M\u00e9ry, D. (ed.) Theoretical Aspects of Computing\u2014ICTAC 2014, Volume 8687 of Lecture Notes in Computer Science. Springer, New York (2014)","DOI":"10.1007\/978-3-319-10882-7_1"},{"issue":"3","key":"249_CR14","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1093\/logcom\/ext016","volume":"26","author":"R Diaconescu","year":"2016","unstructured":"Diaconescu, R.: Quasi-varieties and initial semantics in hybridized institutions. J. Log. Comput. 26(3), 855\u2013891 (2016)","journal-title":"J. Log. Comput."},{"issue":"5","key":"249_CR15","first-page":"1577","volume":"27","author":"R Diaconescu","year":"2017","unstructured":"Diaconescu, R.: Implicit Kripke semantics and ultraproducts in stratified institutions. J. Log. Comput. 27(5), 1577\u20131606 (2017)","journal-title":"J. Log. Comput."},{"issue":"28","key":"249_CR16","doi-asserted-by":"crossref","first-page":"3145","DOI":"10.1016\/j.tcs.2011.04.008","volume":"412","author":"R Diaconescu","year":"2011","unstructured":"Diaconescu, R., \u0162u\u0163u, I.: On the algebra of structured specifications. Theor. Comput. Sci. 412(28), 3145\u20133174 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"249_CR17","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K. : CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, Volume\u00a06 of AMAST Series in Computing. World Scientific, Singapore (1998)","DOI":"10.1142\/3831"},{"key":"249_CR18","unstructured":"Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, Cambridge, 1993, pp. 83\u2013130. Proceedings of a Workshop held in Edinburgh, Scotland (1991)"},{"key":"249_CR19","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1017\/S0960129514000383","volume":"26","author":"R Diaconescu","year":"2016","unstructured":"Diaconescu, R., Madeira, A.: Encoding hybridized institutions into first order logic. Math. Struct. Comput. Sci. 26, 745\u2013788 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"249_CR20","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/j.tcs.2007.02.068","volume":"379","author":"R Diaconescu","year":"2007","unstructured":"Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theor. Comput. Sci. 379(1), 210\u2013230 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"249_CR21","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39(1), 95\u2013146 (1992)","journal-title":"J. Assoc. Comput. Mach."},{"key":"249_CR22","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/s001650200013","volume":"13","author":"J Goguen","year":"2002","unstructured":"Goguen, J., Ro\u015fu, G.: Institution morphisms. Form. Asp. Comput. 13, 274\u2013307 (2002)","journal-title":"Form. Asp. Comput."},{"key":"249_CR23","first-page":"145","volume-title":"Lecture Notes in Mathematics","author":"Alexander Grothendieck","year":"1971","unstructured":"Grothendieck, A.: Cat\u00e9gories fibr\u00e9es et descente. In: Rev\u00eatements \u00e9tales et groupe fondamental, S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9braique du Bois-Marie 1960\/61, Expos\u00e9 VI. Institut des Hautes \u00c9tudes Scientifiques, 1963. Reprinted in Lecture Notes in Mathematics, Volume 224, pp. 145\u201394. Springer, New York (1971)"},{"key":"249_CR24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24, 1\u201315 (1959)","journal-title":"J. Symb. Log."},{"key":"249_CR25","unstructured":"Madeira, A.: Foundations and techniques for software reconfigurability. PhD thesis, Universidades do Minho, Aveiro and Porto (Joint MAP-i Doctoral Programme) (2014)"},{"key":"249_CR26","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-3-642-22944-2_20","volume-title":"Algebra and Coalgebra in Computer Science","author":"Manuel A. Martins","year":"2011","unstructured":"Martins, M.-A., Madeira, A., Diaconescu, R., Barbosa, L.: Hybridization of institutions. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) Algebra and Coalgebra in Computer Science, Volume 6859 of Lecture Notes in Computer Science, pp. 283\u2013297. Springer, New York (2011)"},{"key":"249_CR27","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et\u00a0al. (ed.) Proceedings, Logic Colloquium, 1987, pp. 275\u2013329. North-Holland (1989)","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"249_CR28","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume":"4424","author":"T Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fctich, K.: The heterogeneous tool set. Lect. Notes Comput. Sci. 4424, 519\u2013522 (2007)","journal-title":"Lect. Notes Comput. Sci."},{"key":"249_CR29","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/3-540-61440-0_125","volume-title":"Automata, Languages and Programming","author":"Till Mossakowski","year":"1996","unstructured":"Mossakowski, T.: Different types of arrow between logical frameworks. In: Meyer auf\u00a0der Heide, F., Monien, B. (eds.) Proceedings of ICALP 96, Volume 1099 of Lecture Notes in Computer Science, pp. 158\u2013169. Springer, New York (1996)"},{"key":"249_CR30","unstructured":"Mossakowski, Till: Comorphism-based Grothendieck logics. In K.\u00a0Diks and W.\u00a0Rytter, editors, Mathematical foundations of computer science, volume 2420 of Lecture Notes in Computer Science, pages 593\u2013604. Springer, (2002)"},{"key":"249_CR31","volume-title":"The Road to Universal Logic","author":"T Mossakowski","year":"2015","unstructured":"Mossakowski, T., Codescu, M., Neuhaus, F., Kutz, O.: The distributed ontology, modeling and specification language - dol. In: Buchsbaum, A., Koslow, A. (eds.) The Road to Universal Logic. Birkhauser, Cham (2015)"},{"issue":"2","key":"249_CR32","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0890-5401(91)90026-X","volume":"93","author":"S Passy","year":"1991","unstructured":"Passy, S., Tinchev, T.: An essay in combinatory dynamic logic. Inf. Comput. 93(2), 263\u2013332 (1991)","journal-title":"Inf. Comput."},{"key":"249_CR33","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future","author":"AN Prior","year":"1967","unstructured":"Prior, A.N.: Past, Present and Future. Oxford University Press, Oxford (1967)"},{"issue":"2\u20133","key":"249_CR34","first-page":"91","volume":"15","author":"A Riazonov","year":"2002","unstructured":"Riazonov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"249_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-17336-3","volume-title":"Foundations of Algebraic Specifications and Formal Software Development","author":"D Sannella","year":"2012","unstructured":"Sannella, D., Tarlecki, A.: Foundations of Algebraic Specifications and Formal Software Development. Springer, New York (2012)"},{"key":"249_CR36","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Stephan Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: Proceedings of the 19th conference on Logic Programming and Autamated Reasoning (LPAR), Volume 8312 of LNCS, pp. 477\u2013483 (2013)"},{"key":"249_CR37","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/3-540-61629-2_59","volume-title":"Recent Trends in Data Type Specification","author":"Andrzej Tarlecki","year":"1996","unstructured":"Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.) Recent Trends in Data Type Specification, Volume 1130 of Lecture Notes in Computer Science, pp. 478\u2013502. Springer, New York (1996)"},{"key":"249_CR38","unstructured":"Tarlecki, A.: Towards heterogeneous specifications. In:\u00a0Gabbay, D.,\u00a0van Rijke, M. (eds.) Proceedings, International Conference on Frontiers of Combining Systems (FroCoS\u201998), pp. 337\u2013360. Research Studies Press (2000)"},{"key":"249_CR39","doi-asserted-by":"crossref","first-page":"13","DOI":"10.2307\/2102968","volume":"4","author":"A Tarski","year":"1944","unstructured":"Tarski, A.: The semantic conception of truth. Philos. Phenomenol. Res. 4, 13\u201347 (1944)","journal-title":"Philos. Phenomenol. Res."},{"key":"249_CR40","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-030-30985-5_10","volume-title":"From Software Engineering to Formal Methods and Tools, and Back","author":"Ionu\u0163 \u0162u\u0163u","year":"2019","unstructured":"\u0162u\u0163u, I., Chiri\u0163\u0103, C.E., Lopes, A., Fiadeiro, J.L.: Logical support for bike-sharing system design. In: From Software Engineering to Formal Methods and Tools, and Back, Volume 11865 of Lecture Notes in Computer Science. Springer, New York (2019)"},{"key":"249_CR41","volume-title":"Modal Logic and Classical Logic","author":"J van Bentham","year":"1988","unstructured":"van Bentham, J.: Modal Logic and Classical Logic. Humanities Press, New York (1988)"},{"key":"249_CR42","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"Christoph Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M, Wischnewski, P.: SPASS version 3.5. In: Automated Deduction, Volume 5663 of LNCS, pp. 140\u2013145 (2009)"}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-020-00249-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-020-00249-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-020-00249-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T16:37:30Z","timestamp":1666283850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-020-00249-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,4]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["249"],"URL":"https:\/\/doi.org\/10.1007\/s11787-020-00249-y","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,4]]},"assertion":[{"value":"17 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 March 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 April 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}