{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:57:56Z","timestamp":1769727476220,"version":"3.49.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031212123","type":"print"},{"value":"9783031212130","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-21213-0_11","type":"book-chapter","created":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:08:19Z","timestamp":1670652499000},"page":"169-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Integration of\u00a0Multiple Formal Matrix Models in\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5151-507X","authenticated-orcid":false,"given":"ZhengPu","family":"Shi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1790-2484","authenticated-orcid":false,"given":"Gang","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,11]]},"reference":[{"key":"11_CR1","unstructured":"Zhang, X.D.: Matrix Analysis and Applications, 2nd edn. Tsinghua University Press, Beijing (2013)"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Wang, J., Zhan, N.J., Feng, X.Y., Liu, Z.M.: Overview of formal methods. Ruan Jian Xue Bao\/J. Softw. 30(1), 33\u201361 (2019). (in Chinese with English abstract). https:\/\/doi.org\/10.13328\/j.cnki.jos.005652","DOI":"10.13328\/j.cnki.jos.005652"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Fisher, K., Launchbury, J., Richards, R.: The HACMS program: using formal methods to eliminate exploitable bugs. Philos. Trans. R. Soc. A, 375, 20150401 (2017). https:\/\/doi.org\/10.1098\/rsta.2015.0401","DOI":"10.1098\/rsta.2015.0401"},{"key":"11_CR4","unstructured":"Chen, G., Shi, Z.P.: Formalized engineering mathematics. Commun. CCF 13(10) (2017). (in Chinese with English abstract)"},{"key":"11_CR5","unstructured":"Coq Development Team. The Coq Reference Manual 8.13.2. INRIA (2019)"},{"key":"11_CR6","unstructured":"Isabelle proof assistant. https:\/\/isabelle.in.tum.de"},{"key":"11_CR7","unstructured":"LEAN Theorem Prover: Microsoft Research. https:\/\/leanprover.github.io"},{"key":"11_CR8","unstructured":"The HOL Interactive Theorem Prover. https:\/\/hol-theorem-prover.org"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Ma, Z.W., Chen, G.: Matrix formalization based on Coq record. Comput. Sci. 46(7), 139\u2013145 (2019). (in Chinese with English abstract). https:\/\/doi.org\/10.11896\/j.issn.1002-137X.2019.07.022","DOI":"10.11896\/j.issn.1002-137X.2019.07.022"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Ma. Y.Y., Ma, Z.W., Chen. G.: Formalization of operations of block matrix based on Coq. Ruan Jian Xue Bao\/J. Softw. 32(6), 1882\u20131909 (2021) (in Chinese with English abstract). https:\/\/doi.org\/10.13328\/j.cnki.jos.006255","DOI":"10.13328\/j.cnki.jos.006255"},{"key":"11_CR11","unstructured":"Mathematical Components. https:\/\/math-comp.github.io"},{"key":"11_CR12","unstructured":"Boldo, S., Lelay, C., Melquiond, C.: Coquelicot (2015). https:\/\/coquelicot.saclay.inria.fr\/"},{"key":"11_CR13","unstructured":"Magaud, N.: Programming with Dependent Types in Coq: a Study of Square Matrices (2004). https:\/\/hal.inria.fr\/hal-00955444"},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comp. Sci. 21(4), 827\u2013859 (2011). https:\/\/doi.org\/10.1017\/S0960129511000120","journal-title":"Math. Struct. Comp. Sci."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Hietala, K., Rand, R., Hung, S.-H., Xiaodi, W., Hicks, M.: A verified optimizer for quantum circuits. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL (2021)","DOI":"10.1145\/3434318"},{"key":"11_CR16","unstructured":"Rand, R., Quantum, V.: Computing. Software Foundations Inspired Volume Q. https:\/\/www.cs.umd.edu\/~rrand\/vqc\/index.html"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Geuvers, H., et al.: A constructive algebraic hierarchy in Coq. J. Symbol. Comput. 34(4), 271\u2013286 (2002)","DOI":"10.1006\/jsco.2002.0552"},{"key":"11_CR18","unstructured":"Casteran, P., Sozeau, M.: A Gentle introduction to type classes and relations in Coq (2016)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23"},{"key":"11_CR20","unstructured":"Jung, R.: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies (2019). https:\/\/www.ralfj.de\/blog\/2019\/05\/15\/typeclasses-exponential-blowup.html. Accessed 1 Feb 2022"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Baanen, A.: Use and abuse of instance parameters in the lean mathematical library, 2 May 2022. arXiv, https:\/\/doi.org\/10.48550\/arXiv.2202.01629","DOI":"10.48550\/arXiv.2202.01629"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user (2013). https:\/\/hal.inria.fr\/hal-00816703v1","DOI":"10.1007\/978-3-642-39634-2_5"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-21213-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:15:52Z","timestamp":1670652952000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21213-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212123","9783031212130"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21213-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"11 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2022","order":10,"name":"conference_id","label":"Conference ID","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":"29","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":"11","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":"3","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":"38% - 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":"4","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)"}}]}}