{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:20:56Z","timestamp":1742923256564,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031773815"},{"type":"electronic","value":"9783031773822"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_12","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:44Z","timestamp":1732562804000},"page":"200-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Minuska: Towards a\u00a0Formally Verified Programming Language Framework"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7264-2569","authenticated-orcid":false,"given":"Jan","family":"Tu\u0161il","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6655-7798","authenticated-orcid":false,"given":"Jan","family":"Obdr\u017e\u00e1lek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"12_CR1","unstructured":"Anand, A., et al.: CertiCoq: a verified compiler for Coq. In: CoqPL workshop (2016). https:\/\/api.semanticscholar.org\/CorpusID:9607775"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/S10817-022-09655-X","volume":"67","author":"AW Appel","year":"2023","unstructured":"Appel, A.W., Leroy, X.: Efficient extensional binary tries. J. Autom. Reason. 67(1), 8 (2023). https:\/\/doi.org\/10.1007\/S10817-022-09655-X","journal-title":"J. Autom. Reason."},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Boldo, S., Jourdan, J., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Nannarelli, A., Seidel, P., Tang, P.T.P. (eds.) 21st IEEE Symposium on Computer Arithmetic, ARITH 2013, Austin, TX, USA, April 7-10, 2013, pp. 107\u2013115. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ARITH.2013.30","DOI":"10.1109\/ARITH.2013.30"},{"key":"12_CR4","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":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-03421-4_7","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"X Chen","year":"2018","unstructured":"Chen, X., Ro\u015fu, G.: A language-independent program verification framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 92\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_7"},{"key":"12_CR6","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, June 24-27, 2019, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785675","DOI":"10.1109\/LICS.2019.8785675"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Ro\u015fu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pp. 1133\u20131148. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314601","DOI":"10.1145\/3314221.3314601"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Garavel, H.: The rewrite engines competitions: a rectrospective. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 93\u2013100. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-17502-3_6"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Forster, Y., Sozeau, M., Tabareau, N.: Verified extraction from coq to ocaml. Proc. ACM Program. Lang. 8(PLDI) (2024) https:\/\/doi.org\/10.1145\/3656379","DOI":"10.1145\/3656379"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Hills, M., Serb\u0103nut\u0103, T., Ro\u015fu, G.: A rewrite framework for language definitions and for generation of efficient interpreters. In: Denker, G., Talcott, C.L. (eds.) Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006. Electronic Notes in Theoretical Computer Science, vol.\u00a0176, pp. 215\u2013231. Elsevier (2006). https:\/\/doi.org\/10.1016\/J.ENTCS.2007.06.017","DOI":"10.1016\/J.ENTCS.2007.06.017"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Klein, C., Clements, J., et al.: Run your research: on the effectiveness of lightweight mechanization. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pp. 285\u2013296. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103691","DOI":"10.1145\/2103656.2103691"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Maranget, L.: Compiling pattern matching to good decision trees. In: Proceedings of the 2008 ACM SIGPLAN Workshop on ML, ML \u201908, , pp. 35\u201346. Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1411304.1411311","DOI":"10.1145\/1411304.1411311"},{"key":"12_CR14","unstructured":"Megill, N.D., Wheeler, D.A.: Metamath: a Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina (2019). http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Monniaux, D., Gourdin, L., Boulm\u00e9, S., Lebeltel, O.: Testing a formally verified compiler. In: Prevosto, V., Seceleanu, C. (eds.) Tests and Proofs - 17th International Conference, TAP 2023, Leicester, UK, July 18-19, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14066, pp. 40\u201348. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38828-6_3","DOI":"10.1007\/978-3-031-38828-6_3"},{"issue":"6","key":"12_CR16","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/J.JLAP.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., Serb\u0103nut\u0103, T.: An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/J.JLAP.2010.03.012","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"12_CR17","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P Sewell","year":"2010","unstructured":"Sewell, P., et al.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(1), 71\u2013122 (2010). https:\/\/doi.org\/10.1017\/S0956796809990293","journal-title":"J. Funct. Program."},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Stef\u0103nescu, A., Park, D., Yuwen, S., Li, Y., Ro\u015fu, G.: Semantics-based program verifiers for all languages. In: Visser, E., Smaragdakis, Y. (eds.) 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, October 30 - November 4, 2016, pp. 74\u201391. ACM (2016). https:\/\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The Coq proof assistant (2023). https:\/\/doi.org\/10.5281\/zenodo.8161141","DOI":"10.5281\/zenodo.8161141"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Tu\u0161il, J.: Minuska: Towards a Formally Verified Programming Language Framework, June 2024. https:\/\/doi.org\/10.5281\/zenodo.12599432","DOI":"10.5281\/zenodo.12599432"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Tu\u0161il, J., Bereczky, P., Horp\u00e1csi, D.: Interactive matching logic proofs in Coq. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tarifa, S.L.T. (eds.) Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14446, pp. 139\u2013157. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_10","DOI":"10.1007\/978-3-031-47963-2_10"},{"key":"12_CR22","unstructured":"Tu\u0161il, J., Obdr\u017e\u00e1lek, J.: Minuska: towards a formally verified programming language framework (2024). https:\/\/arxiv.org\/abs\/2409.11530"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:02:53Z","timestamp":1732564973000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}