{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T07:42:01Z","timestamp":1777016521144,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,17]],"date-time":"2010-01-17T00:00:00Z","timestamp":1263686400000},"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":[[2010,1,17]]},"DOI":"10.1145\/1706299.1706329","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T15:15:04Z","timestamp":1263914104000},"page":"237-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":58,"title":["Toward a verified relational database management system"],"prefix":"10.1145","author":[{"given":"Gregory","family":"Malecha","sequence":"first","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avraham","family":"Shinnar","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryan","family":"Wisnesky","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Serge Abiteboul Richard Hull and Victor Vianu. Database Foundations. Addison-Wesley 1995.  Serge Abiteboul Richard Hull and Victor Vianu. Database Foundations. Addison-Wesley 1995."},{"key":"e_1_3_2_1_2_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_1_3_1","volume-title":"Separation and Aliasing. Proc. SPACE","volume":"4","author":"Bornat R.","year":"2004","unstructured":"R. Bornat , C. Calcagno , and P. O Hearn . Local Reasoning , Separation and Aliasing. Proc. SPACE , volume 4 , 2004 . R. Bornat, C. Calcagno, and P. OHearn. Local Reasoning, Separation and Aliasing. Proc. SPACE, volume 4, 2004."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_1_6_1","volume-title":"Introduction to Database Systems","author":"Date C. J.","year":"2002","unstructured":"C. J. Date . Introduction to Database Systems . Addison-Wesley Longman Publishing Co., Inc. , 2002 . C. J. Date. Introduction to Database Systems. Addison-Wesley Longman Publishing Co., Inc., 2002."},{"key":"e_1_3_2_1_7_1","volume-title":"Fundamentals of Database Systems","author":"Elmasri Ramez","year":"2006","unstructured":"Ramez Elmasri and Shamkant B. Navathe . Fundamentals of Database Systems ( 5 th Edition). Addison Wesley , 2006 . Ramez Elmasri and Shamkant B. Navathe. Fundamentals of Database Systems (5th Edition). Addison Wesley, 2006.","edition":"5"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/375663.375749"},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. TYPES","author":"Mcbride Conor","year":"2000","unstructured":"Conor Mcbride . Elimination with a motive . In Proc. TYPES , 2000 . Conor Mcbride. Elimination with a motive. In Proc. TYPES, 2000."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_12_1","volume-title":"J. Functional Programming","author":"Mckinna James","year":"2006","unstructured":"James Mckinna and Joel Wright . A type-correct, stack-safe, provably correct expression compiler in epigram . In J. Functional Programming , 2006 . James Mckinna and Joel Wright. A type-correct, stack-safe, provably correct expression compiler in epigram. In J. Functional Programming, 2006."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481872"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411213"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. WORLDS","author":"Sharon","year":"2006","unstructured":"Sharon E. Perl and Margo Seltzer. Data management for internet-scale single-sign-on . In Proc. WORLDS , 2006 . Sharon E. Perl and Margo Seltzer. Data management for internet-scale single-sign-on. In Proc. WORLDS, 2006."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646056.678061"},{"key":"e_1_3_2_1_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_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.021"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.021"},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. CADE-17","author":"Sinz Carsten","year":"2000","unstructured":"Carsten Sinz . System description : Ara - an automatic theorem prover for relation algebras . In Proc. CADE-17 , 2000 . Carsten Sinz. System description: Ara - an automatic theorem prover for relation algebras. In Proc. CADE-17, 2000."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291156"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Madrid Spain","acronym":"POPL '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706329","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706299.1706329","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:26:19Z","timestamp":1750263979000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706329"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,17]]},"references-count":25,"alternative-id":["10.1145\/1706299.1706329","10.1145\/1706299"],"URL":"https:\/\/doi.org\/10.1145\/1706299.1706329","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1707801.1706329","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,17]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}