{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:37:18Z","timestamp":1759847838025,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031427527"},{"type":"electronic","value":"9783031427534"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-42753-4_12","type":"book-chapter","created":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T06:02:35Z","timestamp":1693375355000},"page":"174-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Morphism Equality in\u00a0Theory Graphs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3379-5922","authenticated-orcid":false,"given":"Franziska","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,28]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-44616-3_5","volume-title":"Recent Trends in Algebraic Development Techniques","author":"S Autexier","year":"2000","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an evolutionary formal software-development using CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73\u201388. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-44616-3_5"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-73228-0_9","volume-title":"Typed Lambda Calculi and Applications","author":"D Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102\u2013117. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73228-0_9"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-319-08434-3_19","volume-title":"Intelligent Computer Mathematics","author":"J Carette","year":"2014","unstructured":"Carette, J., Farmer, W.M., Kohlhase, M.: Realms: a structure for consolidating knowledge about mathematical theories. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 252\u2013266. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_19"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction\u2014CADE-11","author":"WM Farmer","year":"1992","unstructured":"Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567\u2013581. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_192"},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W Farmer","year":"1993","unstructured":"Farmer, W., Guttman, J., Thayer, F.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213\u2013248 (1993)","journal-title":"J. Autom. Reason."},{"key":"12_CR6","unstructured":"Harper, R.: An equational logical framework for type theories (2021). https:\/\/arxiv.org\/abs\/2106.01484"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013165. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_11"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the \u201973 Logic Colloquium, pp. 73\u2013118. North-Holland (1974)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519\u2013522. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_40"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"F Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1\u201354 (2013)","journal-title":"Inf. Comput."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Rabe, F., Sch\u00fcrmann, C.: A practical module system for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40\u201348. ACM Press (2009)","DOI":"10.1145\/1577824.1577831"},{"key":"12_CR14","unstructured":"Rabe, F., Weber, F.: Three case studies on realms. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics, Informal Proceedings, pp. 46\u201351. Research Institute for Symbolic Computation (2022)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-60117-1_22","volume-title":"Mathematics of Program Construction","author":"YV Srinivas","year":"1995","unstructured":"Srinivas, Y.V., J\u00fcllig, R.: Specware: formal support for composing software. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 399\u2013422. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60117-1_22"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/3-540-12689-9_122","volume-title":"Foundations of Computation Theory","author":"D Sannella","year":"1983","unstructured":"Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation extended abstract. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413\u2013427. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/3-540-12689-9_122"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T06:04:01Z","timestamp":1693375441000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-42753-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031427527","9783031427534"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-42753-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"28 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cambridge","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2023\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"52% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}