{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:39Z","timestamp":1763468019343,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198045"},{"type":"electronic","value":"9783642198052"}],"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-19805-2_21","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T09:05:14Z","timestamp":1300093514000},"page":"305-319","source":"Crossref","is-referenced-by-count":2,"title":["A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces"],"prefix":"10.1007","author":[{"given":"Jan","family":"Schwinghammer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristian St","family":"\u00f8 vring","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL (2009)","DOI":"10.1145\/1594834.1480925"},{"issue":"4","key":"21_CR2","first-page":"397","volume":"77","author":"A. Ahmed","year":"2007","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Fundam. Inf.\u00a077(4), 397\u2013449 (2007)","journal-title":"Fundam. Inf."},{"issue":"3","key":"21_CR3","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0022-0000(89)90027-5","volume":"39","author":"P. America","year":"1989","unstructured":"America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci.\u00a039(3), 343\u2013375 (1989)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"21_CR4","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/1275497.1275499","volume":"29","author":"Bodil Biering","year":"2007","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29(5) (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS 2(5:1) (2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"21_CR6","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL (to appear, 2011)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-00596-1_32","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Birkedal","year":"2009","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Realizability semantics of parametric polymorphism, general references, and recursive types. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 456\u2013470. Springer, Heidelberg (2009)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: Proceedings of ICFP, pp. 213\u2013224 (2008)","DOI":"10.1145\/1411203.1411235"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of POPL, pp. 262\u2013275 (1999)","DOI":"10.1145\/292540.292564"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: Proceedings of ICFP (2010)","DOI":"10.1145\/1863543.1863566"},{"key":"21_CR11","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Pilkiewicz, A., Pottier, F.: The essence of monotonic state (July 2010) (unpublished)","DOI":"10.1145\/1929553.1929565"},{"issue":"2","key":"21_CR13","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A.M. Pitts","year":"1996","unstructured":"Pitts, A.M.: Relational properties of domains. Inf. Comput.\u00a0127(2), 66\u201390 (1996)","journal-title":"Inf. Comput."},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In: Proceedings of LICS, pp. 331\u2013340 (2008)","DOI":"10.1109\/LICS.2008.16"},{"key":"21_CR15","unstructured":"Pottier, F.: Generalizing the higher-order frame and anti-frame rules (July 2009) (unpublished), \n                    \n                      http:\/\/gallium.inria.fr\/~fpottier"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-04027-6_32","volume-title":"Computer Science Logic","author":"J. Schwinghammer","year":"2009","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 440\u2013454. Springer, Heidelberg (2009)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12032-9_2","volume-title":"Foundations of Software Science and Computational Structures","author":"J. Schwinghammer","year":"2010","unstructured":"Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B.: A semantic foundation for hidden state. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 2\u201317. Springer, Heidelberg (2010)"},{"key":"21_CR18","volume-title":"Handbook of Logic in Computer Science","author":"M.B. Smyth","year":"1992","unstructured":"Smyth, M.B.: Topology. In: Handbook of Logic in Computer Science, vol.\u00a01. Oxford Univ. Press, Oxford (1992)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T06:29:44Z","timestamp":1558420184000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}