{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:07:59Z","timestamp":1725505679525},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787389"},{"type":"electronic","value":"9783540787396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_26","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:39:06Z","timestamp":1207125546000},"page":"337-352","source":"Crossref","is-referenced-by-count":7,"title":["A Realizability Model for Impredicative Hoare Type Theory"],"prefix":"10.1007","author":[{"given":"Rasmus Lerchedahl","family":"Petersen","sequence":"first","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]},{"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A., Melli\u00e8es, P.-A., Richards, C., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL 2007 (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"26_CR2","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., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/11595014","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"2005","unstructured":"Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 88\u2013101. Springer, Heidelberg (2005)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: Danvy, O., Pierce, B.C. (eds.) ICFP 2005, Tallinn, Estonia, September 2005, pp. 280\u2013293 (2005)","DOI":"10.1145\/1086365.1086401"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: Bi hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"26_CR6","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines, Higher-Order Separation Logic, and Abstraction. In: TOPLAS 2007 (to appear, 2007)"},{"key":"26_CR7","unstructured":"Birkedal, L., M\u00f8gelberg, R., Petersen, R.: Domain-theoretic models of parametric polymorphism. In: TCS (to appear, 2007)"},{"issue":"5:1","key":"26_CR8","first-page":"1","volume":"2","author":"L. Birkedal","year":"2006","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for algol-like languages. LMCS\u00a02(5:1), 1\u201333 (2006)","journal-title":"LMCS"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_8","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Birkedal","year":"2007","unstructured":"Birkedal, L., Yang, H.: Relational parametricity and separation logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, Springer, Heidelberg (2007)"},{"issue":"3","key":"26_CR10","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: 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":"26_CR11","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Compaq Systems Research Center, Research Report 159 (December 1998)"},{"issue":"1","key":"26_CR12","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"},{"key":"26_CR13","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a0141. Elsevier, Amsterdam (1999)"},{"key":"26_CR14","unstructured":"Krishnaswami, N.: Separation logic for a higher-order typed language. In: SPACE 2006, pp. 73\u201382 (2006)"},{"key":"26_CR15","unstructured":"Krishnaswami, N., Aldrich, J., Birkedal, L.: Modular verification of the subject-observer pattern via higher-order separation logic. In: FTfJP (2007)"},{"issue":"3","key":"26_CR16","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM TPLS\u00a021(3), 527\u2013568 (1999)","journal-title":"ACM TPLS"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-71316-6_14","volume-title":"Programming Languages and Systems","author":"A. Nanevski","year":"2007","unstructured":"Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract Predicates and Mutable ADTs in Hoare Type Theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 189\u2013204. Springer, Heidelberg (2007)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. In: ICFP 2006, Portland, Oregon, pp. 62\u201373 (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268\u2013280 (2004)","DOI":"10.1145\/982962.964024"},{"key":"26_CR20","unstructured":"Petersen, R., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model of impredicative hoare type theory. Technical report, IT University of Copenhagen (2007), http:\/\/www.itu.dk\/people\/birkedal\/papers\/httmodel-tr.pdf"},{"key":"26_CR21","series-title":"Applied Logics Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"D. Pym","year":"2002","unstructured":"Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series, vol.\u00a026. Kluwer, Dordrecht (2002)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/11874683_38","volume-title":"Computer Science Logic","author":"B. Reus","year":"2006","unstructured":"Reus, B., Schwinghammer, J.: Separation Logic for Higher-Order Store. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 575\u2013590. Springer, Heidelberg (2006)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"26_CR24","unstructured":"Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, Cambridge University (December 2004)"},{"key":"26_CR25","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.tcs.2005.06.003","volume":"342","author":"M.R. Shinwell","year":"2005","unstructured":"Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. TCS\u00a0342, 28\u201355 (2005)","journal-title":"TCS"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","first-page":"355","volume-title":"Types for Proofs and Programs","author":"K. Watkins","year":"2006","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 355\u2013377. Springer, Heidelberg (2006)"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL 1999, San Antonio, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_26","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Yoshida","year":"2007","unstructured":"Yoshida, N., Honda, K., Berger, M.: Local state in hoare logic for imperative higher-order functions. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:20:50Z","timestamp":1619522450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_26","relation":{},"subject":[]}}