{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:00:17Z","timestamp":1742954417339,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226540"},{"type":"electronic","value":"9783642226557"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22655-7_23","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T13:37:43Z","timestamp":1310996263000},"page":"484-509","source":"Crossref","is-referenced-by-count":9,"title":["Maintaining Database Integrity with Refinement Types"],"prefix":"10.1007","author":[{"given":"Ioannis G.","family":"Baltopoulos","sequence":"first","affiliation":[]},{"given":"Johannes","family":"Borgstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Baltopoulos, I.G., Borgstr\u00f6m, J., Gordon, A.D.: Maintaining database integrity with refinement types. Technical Report MSR\u2013TR\u20132011\u201351, Microsoft Research (2011)","DOI":"10.1007\/978-3-642-22655-7_23"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"issue":"1","key":"23_CR3","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1006\/inco.1998.2731","volume":"147","author":"M. Benedikt","year":"1998","unstructured":"Benedikt, M., Griffin, T., Libkin, L.: Verifiable properties of database transactions. Information and Computation\u00a0147(1), 57\u201388 (1998)","journal-title":"Information and Computation"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/CSF.2008.27","volume-title":"Computer Security Foundations Symposium (CSF 2008)","author":"J. Bengtson","year":"2008","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Computer Security Foundations Symposium (CSF 2008), pp. 17\u201332. IEEE, Los Alamitos (2008)"},{"key":"23_CR5","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF01231645","volume":"4","author":"V. Benzaken","year":"1995","unstructured":"Benzaken, V., Doucet, A.: Th\u00e9mis: A database programming language handling integrity constraints. VLDB Journal\u00a04, 493\u2013517 (1995)","journal-title":"VLDB Journal"},{"key":"23_CR6","first-page":"105","volume-title":"International Conference on Functional Programming (ICFP)","author":"G.M. Bierman","year":"2010","unstructured":"Bierman, G.M., Gordon, A.D., Hri\u0163cu, C., Langworthy, D.: Semantic subtyping with an SMT solver. In: International Conference on Functional Programming (ICFP), pp. 105\u2013116. ACM, New York (2010)"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1596638.1596648","volume-title":"Haskell Symposium","author":"J. Borgstr\u00f6m","year":"2009","unstructured":"Borgstr\u00f6m, J., Bhargavan, K., Gordon, A.D.: A compositional theory for STM Haskell. In: Haskell Symposium, pp. 69\u201380. ACM, New York (2009)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1017\/S0956796810000134","volume":"21","author":"J. Borgstr\u00f6m","year":"2011","unstructured":"Borgstr\u00f6m, J., Gordon, A.D., Pucella, R.: Roles, stacks, histories: A triple for Hoare. Journal of Functional Programming\u00a021, 159\u2013207 (2011); An abridged version of this article was published in A. W. Roscoe, Cliff B. Jones, Kenneth R. Wood (eds.), Reflections on the Work of C.A.R. Hoare, Springer London Ltd (2010)","journal-title":"Journal of Functional Programming"},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1145\/357103.357111","volume":"2","author":"M.A. Casanova","year":"1980","unstructured":"Casanova, M.A., Bernstein, P.A.: A formal system for reasoning about programs accessing a relational database. ACM Transactions on Programming Languages and Systems\u00a02(3), 386\u2013414 (1980)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR10","first-page":"122","volume-title":"Programming Language Design and Implementation (PLDI)","author":"A.J. Chlipala","year":"2010","unstructured":"Chlipala, A.J.: Ur: statically-typed metaprogramming with type-level record computation. In: Programming Language Design and Implementation (PLDI), pp. 122\u2013133. ACM, New York (2010)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-74792-5_12","volume-title":"Formal Methods for Components and Objects","author":"E. Cooper","year":"2007","unstructured":"Cooper, E., Lindley, S., Yallop, J.: Links: Web programming without tiers. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol.\u00a04709, pp. 266\u2013296. Springer, Heidelberg (2007)"},{"key":"23_CR12","first-page":"1403","volume-title":"International Conference on Data Engineering (ICDE)","author":"A. Dasgupta","year":"2009","unstructured":"Dasgupta, A., Narasayya, V.R., Syamala, M.: A static analysis framework for database applications. In: International Conference on Data Engineering (ICDE), pp. 1403\u20131414. IEEE Computer, Los Alamitos (2009)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-48167-2_6","volume-title":"Types for Proofs and Programs","author":"J.-C. Filli\u00e2tre","year":"1999","unstructured":"Filli\u00e2tre, J.-C.: Proof of imperative programs in type theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, pp. 78\u201392. Springer, Heidelberg (1999)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Hybrid type checking. In: ACM Symposium on Principles of Programming Languages (POPL 2006), pp. 245\u2013256 (2006)","DOI":"10.1145\/1111037.1111059"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1109\/VLDB.1979.718144","volume-title":"Fifth International Conference on Very Large Data Bases","author":"G. Gardarin","year":"1979","unstructured":"Gardarin, G., Melkanoff, M.A.: Proving consistency of database transactions. In: Fifth International Conference on Very Large Data Bases, pp. 291\u2013298. IEEE, Los Alamitos (1979)"},{"issue":"4","key":"23_CR17","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s10990-007-9008-y","volume":"20","author":"S. Krishnamurthi","year":"2007","unstructured":"Krishnamurthi, S., Hopkins, P.W., Mccarthy, J., Graunke, P.T., Pettyjohn, G., Felleisen, M.: Implementation and use of the PLT scheme web server. Journal of Higher-Order and Symbolic Computing (HOSC)\u00a020(4), 431\u2013460 (2007)","journal-title":"Journal of Higher-Order and Symbolic Computing (HOSC)"},{"key":"23_CR18","first-page":"237","volume-title":"Principles of Programming Languages (POPL)","author":"J.G. Malecha","year":"2010","unstructured":"Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Principles of Programming Languages (POPL), pp. 237\u2013248. ACM, New York (2010)"},{"key":"23_CR19","first-page":"706","volume-title":"SIGMOD Conference","author":"E. Meijer","year":"2006","unstructured":"Meijer, E., Beckman, B., Bierman, G.M.: LINQ: reconciling object, relations and XML in the.NET framework. In: SIGMOD Conference, p. 706. ACM, New York (2006)"},{"key":"23_CR20","first-page":"229","volume-title":"International Conference on Functional Programming (ICFP 2008)","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: International Conference on Functional Programming (ICFP 2008), pp. 229\u2013240. ACM, New York (2008)"},{"key":"23_CR21","unstructured":"Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala programming language. Technical Report IC\/2004\/64, EPFL (2004)"},{"key":"23_CR22","first-page":"61","volume-title":"Haskell 2007","author":"S. Peyton Jones","year":"2007","unstructured":"Peyton Jones, S., Wadler, P.: Comprehensive comprehensions. In: Haskell 2007, pp. 61\u201372. ACM, New York (2007)"},{"key":"23_CR23","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2 (2006)"},{"key":"23_CR24","first-page":"159","volume-title":"Programming Language Design and Implementation (PLDI)","author":"P. Rondon","year":"2008","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: Programming Language Design and Implementation (PLDI), pp. 159\u2013169. ACM, New York (2008)"},{"key":"23_CR25","first-page":"975","volume-title":"Object-oriented programming systems, languages, and applications (OOPSLA 2006)","author":"M. Serrano","year":"2006","unstructured":"Serrano, M., Gallesio, E., Loitsch, F.: Hop: a language for programming the web 2.0. In: Object-oriented programming systems, languages, and applications (OOPSLA 2006), pp. 975\u2013985. ACM, New York (2006)"},{"issue":"3","key":"23_CR26","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1145\/68012.68014","volume":"14","author":"T. Sheard","year":"1989","unstructured":"Sheard, T., Stemple, D.: Automatic verification of database transaction safety. ACM Transactions on Database Systems\u00a014(3), 322\u2013368 (1989)","journal-title":"ACM Transactions on Database Systems"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-642-11957-6_28","volume-title":"Programming Languages and Systems","author":"N. Swamy","year":"2010","unstructured":"Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 529\u2013549. Springer, Heidelberg (2010)"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Syme, D., Granicz, A., Cisternino, A.: Expert F#. Apress (2007)","DOI":"10.1007\/978-1-4302-0285-1"},{"key":"23_CR29","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P. Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Mathematical Structures in Computer Science\u00a02, 461\u2013493 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-64823-2_2","volume-title":"Database Programming Languages","author":"P. Wadler","year":"1998","unstructured":"Wadler, P.: Functional programming: An angry half-dozen. In: Cluet, S., Hull, R. (eds.) DBPL 1997. LNCS, vol.\u00a01369, pp. 25\u201334. Springer, Heidelberg (1998)"},{"issue":"2","key":"23_CR31","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1017\/S0956796806006216","volume":"17","author":"H. Xi","year":"2007","unstructured":"Xi, H.: Dependent ML: An approach to practical programming with dependent types. Journal of Functional Programming\u00a017(2), 215\u2013286 (2007)","journal-title":"Journal of Functional Programming"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2011 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22655-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T22:30:57Z","timestamp":1560378657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22655-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226540","9783642226557"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22655-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}