{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:27Z","timestamp":1725511887953},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713142"},{"type":"electronic","value":"9783540713166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_14","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:58:28Z","timestamp":1184590708000},"page":"189-204","source":"Crossref","is-referenced-by-count":16,"title":["Abstract Predicates and Mutable ADTs in Hoare Type Theory"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Nanevski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., et al. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, Springer, Heidelberg (2004)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12","volume-title":"Computer Science Logic","author":"N. Benton","year":"2006","unstructured":"Benton, N.: Abstracting Allocation: The New new Thing. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, Springer, Heidelberg (2006)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: ICFP\u201905, pp. 280\u2013293 (2005)","DOI":"10.1145\/1086365.1086401"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines, Higher-Order Separation Logic, and Abstraction. ITU-TR-2005-69, IT University, Copenhagen (2005)","DOI":"10.1007\/978-3-540-31987-0_17"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"DeLine, R., Fahndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI\u201901, pp. 59\u201369 (2001)","DOI":"10.1145\/378795.378811"},{"key":"14_CR8","unstructured":"Detlefs, D.L., et al.: Extended static checking. Compaq Systems Research Center, Research Report 159 (December 1998)"},{"issue":"1","key":"14_CR9","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/52.976940","volume":"19","author":"D. Evans","year":"2002","unstructured":"Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software\u00a019(1), 42\u201351 (2002)","journal-title":"IEEE Software"},{"issue":"4","key":"14_CR10","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.-C.: Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming\u00a013(4), 709\u2013745 (2003)","journal-title":"Journal of Functional Programming"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Inductive definitions: automation and application. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971, Springer, Heidelberg (1995)"},{"key":"14_CR12","unstructured":"Jim, T., et al.: Cyclone: A safe dialect of C. In: USENIX Annual Technical Conference (2002)"},{"key":"14_CR13","unstructured":"Krishnaswami, N.: Separation logic for a higher-order typed language. In: SPACE\u201906 (2006)"},{"key":"14_CR14","unstructured":"Luo, Z.: An Extended Calculus of Constructions. PhD thesis, U.\u00a0of Edinburgh (1990)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: ICFP\u201903, pp. 213\u2013226 (2003)","DOI":"10.1145\/944705.944725"},{"key":"14_CR16","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)"},{"key":"14_CR17","unstructured":"McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)"},{"key":"14_CR18","volume-title":"Foundations for Programming Languages","author":"J.C. Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"issue":"1","key":"14_CR19","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"issue":"3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., et al.: From System F to typed assembly language. TOPLAS\u00a021(3), 527\u2013568 (1999)","journal-title":"TOPLAS"},{"key":"14_CR21","unstructured":"Nanevski, A., et al.: Abstract predicates and mutable ADTs in Hoare Type Theory. TR-14-06, Harvard University (July 2006), Available at http:\/\/www.eecs.harvard.edu\/~aleks\/papers\/hoarelogic\/htthol.pdf"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. In: ICFP\u201906, pp. 62\u201373 (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL\u201906, pp. 320\u2013333 (2006)","DOI":"10.1145\/1111037.1111066"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL\u201904, pp. 268\u2013280 (2004)","DOI":"10.1145\/982962.964024"},{"issue":"1","key":"14_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/345099.345100","volume":"22","author":"B.C. Pierce","year":"2000","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. TOPLAS\u00a022(1), 1\u201344 (2000)","journal-title":"TOPLAS"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS\u201902, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"14_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1053468.1053469","volume":"27","author":"Z. Shao","year":"2005","unstructured":"Shao, Z., et al.: A type system for certified binaries. TOPLAS\u00a027(1), 1\u201345 (2005)","journal-title":"TOPLAS"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"K. Watkins","year":"2004","unstructured":"Watkins, K., et al.: A concurrent logical framework: The propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, Springer, Heidelberg (2004)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"H. Xi","year":"2004","unstructured":"Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, Springer, Heidelberg (2004)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL\u201999 (1999)","DOI":"10.1145\/292540.292560"},{"key":"14_CR31","unstructured":"Yoshida, N., Honda, K., Berger, M.: Logical reasoning for higher-order functions with local state. Personal communication (August 2006)"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","first-page":"83","volume-title":"Practical Aspects of Declarative Languages","author":"H. Xi","year":"2005","unstructured":"Xi, H., Zhu, D.: Safe Programming with Pointers Through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol.\u00a03350, pp. 83\u201397. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71316-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:50:07Z","timestamp":1556668207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}