{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:21:40Z","timestamp":1743060100458,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031212123"},{"type":"electronic","value":"9783031212130"}],"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_13","type":"book-chapter","created":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:08:19Z","timestamp":1670652499000},"page":"205-226","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["LOGIC: A Coq Library for\u00a0Logics"],"prefix":"10.1007","author":[{"given":"Yichen","family":"Tao","sequence":"first","affiliation":[]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,11]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"13_CR2","unstructured":"Appel, A.W.: Verifiable C, chap. 5\u201317, 21, 35\u201339 (2016)"},{"key":"13_CR3","unstructured":"Barras, B., et al.: The coq Proof Assistant reference manual. Technical report, INRIA (1998)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Claus, M., Sultana, N.: Systematic verification of the modal logic cube in Isabelle\/Hol. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2\u20133 August 2015. EPTCS, vol. 186, pp. 27\u201341 (2015), https:\/\/doi.org\/10.4204\/EPTCS.186.5","DOI":"10.4204\/EPTCS.186.5"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-319-20297-6_25","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Interacting with modal logics in the coq proof assistant. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 398\u2013411. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20297-6_25"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-FLOYD: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1\u20134), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5","DOI":"10.1007\/s10817-018-9457-5"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-71237-6_10","volume-title":"Programming Languages and Systems","author":"Q Cao","year":"2017","unstructured":"Cao, Q., Cuellar, S., Appel, A.W.: Bringing order to the separation logic jungle. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 190\u2013211. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_10"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: Morrisett, G., Uustalu, T. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA - 25\u201327 September 2013, pp. 391\u2013402. ACM (2013). https:\/\/doi.org\/10.1145\/2500365.2500592","DOI":"10.1145\/2500365.2500592"},{"key":"13_CR10","series-title":"Undergraduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-73839-6","volume-title":"Mathematical Logic","author":"H Ebbinghaus","year":"1994","unstructured":"Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic. Undergraduate Texts in Mathematics, vol. 291, 2nd edn. Springer, Cham (1994). https:\/\/doi.org\/10.1007\/978-3-030-73839-6","edition":"2"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Forster, Y., Kirst, D., Wehr, D.: Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput. 31(1), 112\u2013151 (2021). https:\/\/doi.org\/10.1093\/logcom\/exaa073","DOI":"10.1093\/logcom\/exaa073"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Forster, Y., Larchey-Wendling, D.: Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14\u201315 January 2019, pp. 104\u2013117. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294096","DOI":"10.1145\/3293880.3294096"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-25379-9_16","volume-title":"Certified Programs and Proofs","author":"M Henz","year":"2011","unstructured":"Henz, M., Hobor, A.: Teaching experience: logic and formal methods with coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 199\u2013215. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_16"},{"key":"13_CR14","unstructured":"Jensen, J.B.: Techniques for model construction in separation logic. Ph.D. thesis, IT University of Copenhagen, March 2014. https:\/\/public.knef.dk.s3-website-us-east-1.amazonaws.com\/research\/sltut.pdf"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL), 66:1\u201366:34 (2018). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Jung, R., et al.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 637\u2013650. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Krebbers, R., et al.: Mosel: a general, extensible modal framework for interactive proofs in separation logic. PACMPL. 2(ICFP), 77:1\u201377:30 (2018). https:\/\/doi.org\/10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"13_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-7288-6","volume-title":"Introduction to Mathematical Logic","author":"E Mendelson","year":"1987","unstructured":"Mendelson, E.: Introduction to Mathematical Logic, 3rd edn. Chapman and Hall, London (1987)","edition":"3"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541"},{"key":"13_CR20","unstructured":"Pierce, B.C., et al.: Software foundations. Webpage: https:\/\/wwwcis.upenn.edu\/bcpierce\/sf\/current\/index.html (2010)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-22102-1_25","volume-title":"Interactive Theorem Proving","author":"F Sieczkowski","year":"2015","unstructured":"Sieczkowski, F., Bizjak, A., Birkedal, L.: ModuRes: a COQ library for modular reasoning about concurrent higher-order imperative programming languages. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 375\u2013390. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_25"},{"key":"13_CR22","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":"13_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-40537-2_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"H Tews","year":"2013","unstructured":"Tews, H.: Formalizing cut elimination of coalgebraic logics in COQ. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 257\u2013272. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40537-2_22"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:15:36Z","timestamp":1670652936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21213-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212123","9783031212130"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21213-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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)"}}]}}