{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:20:41Z","timestamp":1758709241986,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031479625"},{"type":"electronic","value":"9783031479632"}],"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-47963-2_10","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:26Z","timestamp":1700689286000},"page":"139-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Interactive Matching Logic Proofs in\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7264-2569","authenticated-orcid":false,"given":"Jan","family":"Tu\u0161il","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3183-0712","authenticated-orcid":false,"given":"P\u00e9ter","family":"Bereczky","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0261-0091","authenticated-orcid":false,"given":"D\u00e1niel","family":"Horp\u00e1csi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,23]]},"reference":[{"key":"10_CR1","unstructured":"Matching logic formalization. https:\/\/github.com\/harp-project\/AML-Formalization\/releases\/tag\/v1.0.15. Accessed 27 June 2023"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Investigations into logical deduction. In: Szabo, M. (ed.) The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. Elsevier (1969). https:\/\/doi.org\/10.1016\/S0049-237X(08)70822-X","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5\u201321. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_3"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bereczky, P., Chen, X., Horp\u00e1csi, D., Pe\u00f1a, L., Tu\u0161il, J.: Mechanizing matching logic in Coq. Electronic Proceedings in Theoretical Computer Science (2022). https:\/\/doi.org\/10.4204\/eptcs.369.2","DOI":"10.4204\/eptcs.369.2"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3018610.3018616","DOI":"10.1145\/3018610.3018616"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Bornat, R., Sufrin, B.: Animating formal proof at the surface: the Jape Proof Calculator. Comput. J. (1999). https:\/\/doi.org\/10.1093\/comjnl\/42.3.177","DOI":"10.1093\/comjnl\/42.3.177"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic. Studies in Logic and Practical Reasoning. Elsevier (2007). https:\/\/doi.org\/10.1016\/S1570-2464(07)80015-2","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. (2012). https:\/\/doi.org\/10.1007\/s10817-011-9225-2","DOI":"10.1007\/s10817-011-9225-2"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-030-81688-9_23","volume-title":"Computer Aided Verification","author":"X Chen","year":"2021","unstructured":"Chen, X., Lin, Z., Trinh, M.-T., Ro\u015fu, G.: Towards a trustworthy semantics-based language framework via proof generation. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 477\u2013499. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_23"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Chen, X., Lucanu, D., Rosu, G.: Capturing constrained constructor patterns in matching logic. J. Log. Algebraic Methods Program. (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2022.100810","DOI":"10.1016\/j.jlamp.2022.100810"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Chen, X., Lucanu, D., Ro\u015fu, G.: Matching logic explained. J. Logical Algebraic Methods Program. (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2021.100638","DOI":"10.1016\/j.jlamp.2021.100638"},{"key":"10_CR12","unstructured":"Chen, X., Ro\u015fu, G.: Applicative matching logic: semantics of K. Technical report, University of Illinois at Urbana-Champaign (2019). http:\/\/hdl.handle.net\/2142\/104616"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Chen, X., Ro\u015fu, G.: Matching $$\\mu $$-logic. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, 24\u201327 June 2019. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785675","DOI":"10.1109\/LICS.2019.8785675"},{"key":"10_CR14","unstructured":"Chen, X., Ro\u015fu, G.: Matching mu-logic. Technical report, University of Illinois at Urbana-Champaign (2019). http:\/\/hdl.handle.net\/2142\/102281. Accessed 16 Feb 2023"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Cheney, J., Fernandez, M.: Nominal matching logic. In: Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3551357.3551375","DOI":"10.1145\/3551357.3551375"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Coupet-Grimal, S.: An axiomatization of linear temporal logic in the Calculus of Inductive Constructions. J. Log. Comput. (2003). https:\/\/doi.org\/10.1093\/logcom\/13.6.801","DOI":"10.1093\/logcom\/13.6.801"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Logic (1992). https:\/\/doi.org\/10.2307\/2275431","DOI":"10.2307\/2275431"},{"key":"10_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3"},{"key":"10_CR19","doi-asserted-by":"publisher","DOI":"10.1145\/3236772","author":"R Krebbers","year":"2018","unstructured":"Krebbers, R., et al.: MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. (2018). https:\/\/doi.org\/10.1145\/3236772","journal-title":"Proc. ACM Program. Lang."},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-031-17715-6_19","volume-title":"Theoretical Aspects of Computing","author":"AI Lungu","year":"2022","unstructured":"Lungu, A.I., Lucanu, D.: A matching logic foundation for Alk. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC 2022. LNCS, vol. 13572, pp. 290\u2013304. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_19"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Theorem Proving in Higher Order Logics","author":"A McCreight","year":"2009","unstructured":"McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 343\u2013358. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_24"},{"key":"10_CR23","unstructured":"Megill, N., Wheeler, D.A.: Metamath: a computer language for mathematical proofs. http:\/\/us.metamath.org. Accessed 16 Feb 2023"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29 May\u20131 June 2017. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2017.5","DOI":"10.4230\/LIPIcs.TYPES.2017.5"},{"key":"10_CR25","unstructured":"Pelletier, F.J., Hazen, A.: Natural deduction systems in logic. In: The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University (2022)"},{"key":"10_CR26","unstructured":"Power, J.F., Webster, C.: Working with linear logic in Coq (1999). https:\/\/mural.maynoothuniversity.ie\/6461\/1\/JP-Working-Linear-Logic.pdf. Accessed 16 Feb 2023"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G.: Matching logic. Log. Methods Comput. Sci. (2017). https:\/\/doi.org\/10.23638\/LMCS-13(4:28)2017","DOI":"10.23638\/LMCS-13(4:28)2017"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, Part of SPLASH 2016, Amsterdam, The Netherlands, 30 October\u20134 November 2016. ACM (2016). https:\/\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The coq proof assistant (2022). https:\/\/doi.org\/10.5281\/zenodo.7313584","DOI":"10.5281\/zenodo.7313584"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Wang, S.B., Dong, W.Y.: Matching logic for concurrent programs based on rely\/guarantee and abstract patterns. Int. J. Softw. Eng. Knowl. Eng. (2022)","DOI":"10.1142\/S0218194022500759"},{"key":"10_CR31","unstructured":"Wiedijk, F.: Encoding the HOL Light logic in Coq (2007). https:\/\/www.cs.ru.nl\/~freek\/notes\/holl2coq.pdf. Accessed 30 June 2023"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47963-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:42:32Z","timestamp":1700689352000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47963-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031479625","9783031479632"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47963-2_10","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":"23 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Peru","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 December 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2023.compsust.utec.edu.pe\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}