{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:13:11Z","timestamp":1770279191049,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"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,1,20]]},"DOI":"10.1145\/1481848.1481856","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"49-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Verified programming in Guru"],"prefix":"10.1145","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[{"name":"The University of Iowa, Iowa City, IA, USA"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[{"name":"Technical University of Catalonia, Barcelona, Spain"}]},{"given":"Adam","family":"Petcher","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, St. Louis, MO, USA"}]},{"given":"Todd","family":"Schiller","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, St. Louis, MO, USA"}]},{"given":"Timothy","family":"Simpson","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, St. Louis, MO, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Foundational Proof-Carrying Code. In 16th Annual IEEE Symposium on Logic in Computer Science","author":"Appel A.","year":"2001","unstructured":"A. Appel . Foundational Proof-Carrying Code. In 16th Annual IEEE Symposium on Logic in Computer Science , 2001 . A. Appel. Foundational Proof-Carrying Code. In 16th Annual IEEE Symposium on Logic in Computer Science, 2001."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646831.707715"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07)","author":"Barrett C.","year":"2007","unstructured":"C. Barrett and C. Tinelli . CVC3. In W. Damm and H. Hermanns, editors , Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07) , pages 298 -- 302 . Springer-Verlag , 2007 . C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07), pages 298--302. Springer-Verlag, 2007."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094836"},{"key":"e_1_3_2_1_7_1","first-page":"83","volume-title":"Twenty-five years of constructive type theory","author":"Hofmann M.","year":"1998","unstructured":"M. Hofmann and T. Streicher . The groupoid interpretation of type theory . In G. Sambin, editor, Twenty-five years of constructive type theory , pages 83 -- 111 . Oxford : Clarendon Press , 1998 . M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In G. Sambin, editor, Twenty-five years of constructive type theory, pages 83--111. Oxford: Clarendon Press, 1998."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792784"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_14_1","volume-title":"Chalmers University of Technology","author":"Norell U.","year":"2007","unstructured":"U. Norell . Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis , Chalmers University of Technology , 2007 . U. Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_3_2_1_16_1","volume-title":"Deciding Joinability Modulo Ground Equations in Operational Type Theory. Master's thesis","author":"Petcher A.","year":"2008","unstructured":"A. Petcher . Deciding Joinability Modulo Ground Equations in Operational Type Theory. Master's thesis , Washington University in Saint Louis, May 2008 . Available from http:\/\/cl.cse.wustl.edu. A. Petcher. Deciding Joinability Modulo Ground Equations in Operational Type Theory. Master's thesis, Washington University in Saint Louis, May 2008. Available from http:\/\/cl.cse.wustl.edu."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753634"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.040"},{"key":"e_1_3_2_1_20_1","volume-title":"Logical Frameworks and Meta-Languages: Theory and Practice","author":"Stump A.","year":"2008","unstructured":"A. Stump . Proof Checking Technology for Satisfiability Modulo Theories. In A. Abel and C. Urban, editors , Logical Frameworks and Meta-Languages: Theory and Practice , 2008 . A. Stump. Proof Checking Technology for Satisfiability Modulo Theories. In A. Abel and C. Urban, editors, Logical Frameworks and Meta-Languages: Theory and Practice, 2008."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1512464.1512470"},{"key":"e_1_3_2_1_22_1","unstructured":"A. Stump and E. Westbrook. A Core Operational Type Theory. Under review available from http:\/\/www.cs.uiowa.edu\/ astump.  A. Stump and E. Westbrook. A Core Operational Type Theory. Under review available from http:\/\/www.cs.uiowa.edu\/ astump."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_3_2_1_24_1","volume-title":"Version V8.0","author":"Development Team The Coq","year":"2004","unstructured":"The Coq Development Team . The Coq Proof Assistant Reference Manual , Version V8.0 , 2004 . http:\/\/coq.inria.fr. The Coq Development Team. The Coq Proof Assistant Reference Manual, Version V8.0, 2004. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.29"},{"key":"e_1_3_2_1_27_1","volume-title":"Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)","author":"Zeller M.","year":"2007","unstructured":"M. Zeller , A. Stump , and M. Deters . Signature Compilation for the Edinburgh Logical Framework. In C. Sch\u00fcrmann, editor , Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) , 2007 . M. Zeller, A. Stump, and M. Deters. Signature Compilation for the Edinburgh Logical Framework. In C. Sch\u00fcrmann, editor, Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2007."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 3rd workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481856","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481848.1481856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":25,"alternative-id":["10.1145\/1481848.1481856","10.1145\/1481848"],"URL":"https:\/\/doi.org\/10.1145\/1481848.1481856","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}