{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:08:27Z","timestamp":1750306107183,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,4]],"date-time":"2017-09-04T00:00:00Z","timestamp":1504483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,4]]},"DOI":"10.1145\/3139903.3139905","type":"proceedings-article","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T13:24:32Z","timestamp":1511789072000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Programming a Smalltalk VM in Coq"],"prefix":"10.1145","author":[{"given":"Boris","family":"Shingarov","sequence":"first","affiliation":[{"name":"LabWare"}]}],"member":"320","published-online":{"date-parts":[[2017,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"D. Aarno and J. Engblom. 2015. Software and System Development Using Virtual Platforms. Elsevier.   D. Aarno and J. Engblom. 2015. Software and System Development Using Virtual Platforms. Elsevier.","DOI":"10.1016\/B978-0-12-800725-9.00006-8"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Robert Atkey. 2008. CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. Springer Berlin Heidelberg Berlin Heidelberg 18--32.  Robert Atkey. 2008. CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. Springer Berlin Heidelberg Berlin Heidelberg 18--32.","DOI":"10.1007\/978-3-540-68103-8_2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBAC-PAD.2012.33"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Springer Berlin Heidelberg.   Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2006.82"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814228.2814234"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800542"},{"key":"e_1_3_2_1_9_1","unstructured":"J. Fridstrom A. Jacques K. Kilpela and J. Sarkela. 2014. Modtalk. In 8th Smalltalks -- Argentina Conference. Argentina C\u00f3rdoba.  J. Fridstrom A. Jacques K. Kilpela and J. Sarkela. 2014. Modtalk. In 8th Smalltalks -- Argentina Conference. Argentina C\u00f3rdoba."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"J. Fridstrom A. Jacques K. Kilpela and J. Sarkela. 2015. Testing Modtalk. In Lecture Notes in Business Information Processing Agile Processes in Software Engineering and Extreme Programming -- 16th International Conference XP. Helsinki Finland.  J. Fridstrom A. Jacques K. Kilpela and J. Sarkela. 2015. Testing Modtalk. In Lecture Notes in Business Information Processing Agile Processes in Software Engineering and Extreme Programming -- 16th International Conference XP. Helsinki Finland.","DOI":"10.1007\/978-3-319-18612-2_30"},{"key":"e_1_3_2_1_11_1","unstructured":"M. Kaufmann P. Manolios and J.S. Moore. 2000. ACL2 Case Studies. Volume 2 of Advances in Formal Methods {13}.  M. Kaufmann P. Manolios and J.S. Moore. 2000. ACL2 Case Studies. Volume 2 of Advances in Formal Methods {13}."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"M. Kaufmann P. Manolios and J.S. Moore. 2000. An Approach. Volume 1 of Advances in Formal Methods {13}.  M. Kaufmann P. Manolios and J.S. Moore. 2000. An Approach. Volume 1 of Advances in Formal Methods {13}.","DOI":"10.1007\/978-1-4615-4449-4_1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"M. Kaufmann P. Manolios and J.S. Moore. 2000. Computer-Aided Reasoning. (2000).   M. Kaufmann P. Manolios and J.S. Moore. 2000. Computer-Aided Reasoning. (2000).","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682930"},{"key":"e_1_3_2_1_17_1","unstructured":"Xavier Leroy. 2017. The CompCert C verified compiler. INRIA Paris.  Xavier Leroy. 2017. The CompCert C verified compiler. INRIA Paris."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/858570.858572"},{"volume-title":"Mathematical Aspects of Computer Science (Proceedings of Symposia in Applied Mathematics)","author":"McCarthy John","key":"e_1_3_2_1_20_1"},{"key":"e_1_3_2_1_21_1","unstructured":"Robin Milner and Richard Weyhrauch. 1972. Proving compiler correctness in a mechanized logic. (1972).  Robin Milner and Richard Weyhrauch. 1972. Proving compiler correctness in a mechanized logic. (1972)."},{"key":"e_1_3_2_1_22_1","unstructured":"J Strother Moore. 1996. Piton: a Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers.   J Strother Moore. 1996. Piton: a Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_25"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"e_1_3_2_1_25_1","unstructured":"Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning volumes 1 2. Elsevier Science Publishers B. V. Amsterdam The Netherlands.   Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning volumes 1 2. Elsevier Science Publishers B. V. Amsterdam The Netherlands."},{"volume-title":"Modern Problems for the Smalltalk VM. In International Workshop on Smalltalk Technologies","year":"2014","author":"Shingarov B.","key":"e_1_3_2_1_26_1"},{"volume-title":"8th Smalltalks --- Argentina Conference. Argentina, C\u00f3rdoba.","author":"Shingarov B.","key":"e_1_3_2_1_27_1"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2811237.2811295"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"IWST '17: International Workshop on Smalltalk Technologies","sponsor":["ESUG","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Maribor Slovenia","acronym":"IWST '17"},"container-title":["Proceedings of the 12th edition of the International Workshop on Smalltalk Technologies"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3139903.3139905","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3139903.3139905","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:39Z","timestamp":1750217439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3139903.3139905"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,4]]},"references-count":29,"alternative-id":["10.1145\/3139903.3139905","10.1145\/3139903"],"URL":"https:\/\/doi.org\/10.1145\/3139903.3139905","relation":{},"subject":[],"published":{"date-parts":[[2017,9,4]]},"assertion":[{"value":"2017-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}