乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:18:21Z","timestamp":1725851901205},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_28","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"727-751","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Transfinite Step-Indexing: Decoupling Concrete and Logical Steps"],"prefix":"10.1007","author":[{"given":"Kasper","family":"Svendsen","sequence":"first","affiliation":[]},{"given":"Filip","family":"Sieczkowski","sequence":"additional","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"issue":"1","key":"28_CR2","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/1594834.1480925","volume":"44","author":"Amal Ahmed","year":"2009","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR3","unstructured":"Ahmed, A.J.: Semantics of types for mutable state. Ph.D. thesis, Princeton University (2004)"},{"key":"28_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Dodds, J., Leroy, X., Blazy, S., Stewart, G., Beringer, L.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"issue":"5","key":"28_CR5","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"AW Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Melli\u00e8s, P.-A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of POPL (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.-K.: Biorthogonality, step-indexing and compiler correctness. In: Proceedings of ICFP (2009)","DOI":"10.1145\/1596550.1596567"},{"issue":"4","key":"28_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(4:4)2013","volume":"9","author":"L Birkedal","year":"2013","unstructured":"Birkedal, L., Bizjak, A., Schwinghammer, J.: Step-indexed relational reasoning for countable nondeterminism. Log. Methods Comput. Sci. 9(4), 1\u201323 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4), (2012) \n http:\/\/www.lmcs-online.org\/ojs\/viewarticle.php?id=1118&layout=abstract","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed kripke models over recursive worlds. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"28_CR11","unstructured":"Birkedal, L., Sieczkowski, F., Thamsborg, J.: A concurrent logical relation. In: Proceedings of CSL (2012)"},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"4102","DOI":"10.1016\/j.tcs.2010.07.010","volume":"411","author":"L Birkedal","year":"2010","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Theor. Comput. Sci. 411, 4102\u20134122 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-39185-1_9","volume-title":"Types for Proofs and Programs","author":"P Gianantonio Di","year":"2003","unstructured":"Di Gianantonio, P., Miculan, M.: A unifying approach to recursive and co-recursive definitions. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 148\u2013161. Springer, Heidelberg (2003)"},{"issue":"2","key":"28_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2818638","volume":"38","author":"M Dodds","year":"2016","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J., Svendsen, K., Birkedal, L.: Verifying custom synchronization constructs using higher-order separation logic. ACM Trans. Program. Lang. Syst. 38(2), 1\u201372 (2016)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR15","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1017\/S095679681200024X","volume":"22","author":"D Dreyer","year":"2012","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. J. Funct. Prog. 22, 477\u2013528 (2012)","journal-title":"J. Funct. Prog."},{"issue":"1","key":"28_CR16","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/1707801.1706322","volume":"45","author":"Aquinas Hobor","year":"2010","unstructured":"Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of POPL (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Hur, C.-K., Dreyer, D.: A kripke logical relation between ML and assembly. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926402"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of POPL (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"28_CR19","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS (2002)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: Proceedings of ICFP (2013)","DOI":"10.1145\/2500365.2500600"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: Proceedings of POPL (2013)","DOI":"10.1145\/2429069.2429111"}],"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-662-49498-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T01:05:45Z","timestamp":1584925545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}