{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:53Z","timestamp":1781172353752,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":14,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T00:00:00Z","timestamp":1327449600000},"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":[[2012,1,25]]},"DOI":"10.1145\/2103656.2103691","type":"proceedings-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T11:47:19Z","timestamp":1327405639000},"page":"285-296","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":58,"title":["Run your research"],"prefix":"10.1145","author":[{"given":"Casey","family":"Klein","sequence":"first","affiliation":[{"name":"Northwestern University & PLT, Evanston, IL, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Clements","sequence":"additional","affiliation":[{"name":"California Polytechnic State University & PLT, San Luis Obispo & PLT, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christos","family":"Dimoulas","sequence":"additional","affiliation":[{"name":"Northeastern University & PLT, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carl","family":"Eastlund","sequence":"additional","affiliation":[{"name":"Northeastern University & PLT, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Felleisen","sequence":"additional","affiliation":[{"name":"Northeastern University & PLT, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Flatt","sequence":"additional","affiliation":[{"name":"University of Utah & PLT, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jay A.","family":"McCarthy","sequence":"additional","affiliation":[{"name":"Brigham Young University & PLT, Provo, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jon","family":"Rafkind","sequence":"additional","affiliation":[{"name":"University of Utah & PLT, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sam","family":"Tobin-Hochstadt","sequence":"additional","affiliation":[{"name":"Northeastern University & PLT, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert Bruce","family":"Findler","sequence":"additional","affiliation":[{"name":"Northwestern University, Evanston, IL, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,1,25]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985795"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596589"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273931"},{"key":"e_1_3_2_2_6_1","series-title":"Lecture Notes in Computer Science","first-page":"269","volume-title":"Proc. Intl. Conf. Logic Programming","author":"Cheney James","year":"2004","unstructured":"James Cheney and Christian Urban . \u03b1Prolog: a logic programming language with names, binding, and \u03b1-equivalence . In Proc. Intl. Conf. Logic Programming , Lecture Notes in Computer Science volume 3132 , pp. 269 -- 283 , 2004 . James Cheney and Christian Urban. \u03b1Prolog: a logic programming language with names, binding, and \u03b1-equivalence. In Proc. Intl. Conf. Logic Programming, Lecture Notes in Computer Science volume 3132, pp. 269--283, 2004."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_2_8_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Intl. Conf. Rewriting Techniques and Applications","author":"Clavel Manuel","year":"2003","unstructured":"Manuel Clavel , Francisco Duran , Steven Eker , Patrick Lincoln , Narciso Martin-Oliet , Jose Meseguer , and Carolyn Talcott . Maude 2.0 system. In Proc . Intl. Conf. Rewriting Techniques and Applications , Lecture Notes in Computer Science volume 2706 , pp. 76 -- 87 , 2003 . Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Martin-Oliet, Jose Meseguer, and Carolyn Talcott. Maude 2.0 system. In Proc. Intl. Conf. Rewriting Techniques and Applications, Lecture Notes in Computer Science volume 2706, pp. 76--87, 2003."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651947"},{"key":"e_1_3_2_2_10_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/3-540-13346-1_11","volume-title":"Proc. Intl. Symp. Semantics of Data Types","author":"Despeyroux Thierry","year":"1984","unstructured":"Thierry Despeyroux . Executable specification of static semantics . In Proc. Intl. Symp. Semantics of Data Types , Lecture Notes in Computer Science volume 173 , pp. 215 -- 233 , 1984 . Thierry Despeyroux. Executable specification of static semantics. In Proc. Intl. Symp. Semantics of Data Types, Lecture Notes in Computer Science volume 173, pp. 215--233, 1984."},{"key":"e_1_3_2_2_11_1","volume-title":"Research Report No. 94","author":"Despeyroux Thierry","year":"1988","unstructured":"Thierry Despeyroux . Typol : a formalism to implement natural semantics. INRIA , Research Report No. 94 , 1988 . Thierry Despeyroux. Typol: a formalism to implement natural semantics. INRIA, Research Report No. 94, 1988."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_4"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181787"},{"key":"e_1_3_2_2_14_1","volume-title":"An Executable Formal Semantics of C with Applications","author":"Ellison Chucky","year":"2011","unstructured":"Chucky Ellison and Grigore Rosu . An Executable Formal Semantics of C with Applications . University of Illinois , http:\/\/hdl.handle.net\/2142\/25816, 2011 .. Chucky Ellison and Grigore Rosu. An Executable Formal Semantics of C with Applications. University of Illinois, http:\/\/hdl.handle.net\/2142\/25816, 2011.."}],"event":{"name":"POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Philadelphia PA USA","acronym":"POPL '12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103691","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2103656.2103691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:06:21Z","timestamp":1750226781000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103691"}},"subtitle":["on the effectiveness of lightweight mechanization"],"short-title":[],"issued":{"date-parts":[[2012,1,25]]},"references-count":14,"alternative-id":["10.1145\/2103656.2103691","10.1145\/2103656"],"URL":"https:\/\/doi.org\/10.1145\/2103656.2103691","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2103621.2103691","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,1,25]]},"assertion":[{"value":"2012-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}