{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:27Z","timestamp":1774837827486,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,8,31]],"date-time":"2009-08-31T00:00:00Z","timestamp":1251676800000},"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":[[2009,8,31]]},"DOI":"10.1145\/1596550.1596565","type":"proceedings-article","created":{"date-parts":[[2009,9,1]],"date-time":"2009-09-01T13:53:09Z","timestamp":1251813189000},"page":"79-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":56,"title":["Effective interactive proofs for higher-order imperative programs"],"prefix":"10.1145","author":[{"given":"Adam","family":"Chlipala","sequence":"first","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}]},{"given":"Gregory","family":"Malecha","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}]},{"given":"Avraham","family":"Shinnar","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}]},{"given":"Ryan","family":"Wisnesky","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,8,31]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Proc. CASSIS","author":"Barnett Mike","year":"2004","unstructured":"Mike Barnett , K. Rustan M. Leino , and Wolfram Schulte . The Spec# programming system : An overview . In Proc. CASSIS , 2004 . Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Proc. CASSIS, 2004."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science . Springer Verlag , 2004 . Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411235"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765236.1765246"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964011"},{"key":"e_1_3_2_2_11_1","volume-title":"Proc. Scheme Workshop","author":"Gronski Jessica","year":"2006","unstructured":"Jessica Gronski , Kenneth Knowles , Aaron Tomb , Stephen N. Freund , and Cormac Flanagan . Sage : Hybrid checking for flexible specifications . In Proc. Scheme Workshop , 2006 . Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Proc. Scheme Workshop, 2006."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312816"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_2_17_1","volume-title":"Proc. ICFP","author":"Nanevski Aleksandar","year":"2008","unstructured":"Aleksandar Nanevski , Greg Morrisett , Avraham Shinnar , Paul Govereau , and Lars Birkedal . Ynot : Reasoning with the awkward squad . In Proc. ICFP , 2008 . Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Reasoning with the awkward squad. In Proc. ICFP, 2008."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_3_2_2_20_1","first-page":"5","article-title":"A generic theorem prover","author":"Paulson Lawrence C","year":"1994","unstructured":"Lawrence C Paulson . Isabelle : A generic theorem prover . Journal of Automated Reasoning , 5 , 1994 . Lawrence C Paulson. Isabelle: A generic theorem prover. Journal of Automated Reasoning, 5, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792913"},{"key":"e_1_3_2_2_22_1","volume-title":"Proc. LICS","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . Separation logic : A logic for shared mutable data structures . In Proc. LICS , 2002 . John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, 2002."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"event":{"name":"ICFP '09: ACM SIGPLAN International Conference on Functional Programming","location":"Edinburgh Scotland","acronym":"ICFP '09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 14th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1596550.1596565","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1596550.1596565","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:23:28Z","timestamp":1750235008000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1596550.1596565"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,31]]},"references-count":24,"alternative-id":["10.1145\/1596550.1596565","10.1145\/1596550"],"URL":"https:\/\/doi.org\/10.1145\/1596550.1596565","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1631687.1596565","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,8,31]]},"assertion":[{"value":"2009-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}