{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:55:24Z","timestamp":1770296124843,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_17","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"475-501","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Reasoning About a Machine with Local Capabilities"],"prefix":"10.1007","author":[{"given":"Lau","family":"Skorstengaard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"5","key":"17_CR1","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/173668.168635","volume":"27","author":"Robert Wahbe","year":"1993","unstructured":"Wahbe, R., Lucco, S., Anderson, T.E., Graham, S.L.: Efficient software-based fault isolation. In: Symposium on Operating Systems Principles, pp. 203\u2013216. ACM (1993)","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Budiu, M., Erlingsson, \u00da., Ligatti, J.: Control-flow integrity. In: Conference on Computer and Communications Security, pp. 340\u2013353. ACM (2005)","DOI":"10.1145\/1102120.1102165"},{"issue":"3","key":"17_CR3","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 Trans. Program. Lang. Syst. 21(3), 527\u2013568 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR4","volume-title":"The Java Virtual Machine Specification","author":"T Lindholm","year":"2014","unstructured":"Lindholm, T., Yellin, F., Bracha, G., Buckley, A.: The Java Virtual Machine Specification. Pearson Education, London (2014)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Forrest, S., Somayaji, A., Ackley, D.H.: Building diverse computer systems. In: Hot Topics in Operating Systems, pp. 67\u201372, May 1997","DOI":"10.1109\/HOTOS.1997.595185"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Carter, N.P., Keckler, S.W., Dally, W.J.: Hardware support for fast capability-based addressing. In: Architectural Support for Programming Languages and Operating Systems, pp. 319\u2013327. ACM (1994)","DOI":"10.1145\/195473.195579"},{"issue":"3","key":"17_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/365230.365252","volume":"9","author":"JB Dennis","year":"1966","unstructured":"Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. Commun. ACM 9(3), 143\u2013155 (1966)","journal-title":"Commun. ACM"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Shapiro, J.S., Smith, J.M., Farber, D.J.: EROS: a fast capability system. In: Symposium on Operating Systems Principles, SOSP 1999, pp. 170\u2013185. ACM (1999)","DOI":"10.1145\/319151.319163"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Watson, R.N.M., Woodruff, J., Neumann, P.G., Moore, S.W., Anderson, J., Chisnall, D., Dave, N., Davis, B., Gudka, K., Laurie, B., Murdoch, S.J., Norton, R., Roe, M., Son, S., Vadera, M.: CHERI: a hybrid capability-system architecture for scalable software compartmentalization. In: IEEE Symposium on Security and Privacy, pp. 20\u201337 (2015)","DOI":"10.1109\/SP.2015.9"},{"issue":"3","key":"17_CR10","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1145\/2678373.2665740","volume":"42","author":"Jonathan Woodruff","year":"2014","unstructured":"Woodruff, J., Watson, R.N., Chisnall, D., Moore, S.W., Anderson, J., Davis, B., Laurie, B., Neumann, P.G., Norton, R., Roe, M.: The CHERI capability model: revisiting RISC in an age of risk. In: International Symposium on Computer Architecture, pp. 457\u2013468. IEEE Press (2014)","journal-title":"ACM SIGARCH Computer Architecture News"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Devriese, D., Birkedal, L., Piessens, F.: Reasoning about object capabilities using logical relations and effect parametricity. In: IEEE European Symposium on Security and Privacy. IEEE (2016)","DOI":"10.1109\/EuroSP.2016.22"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Maffeis, S., Mitchell, J., Taly, A.: Object capabilities and isolation of untrusted web applications. In: S&P, pp. 125\u2013140. IEEE (2010)","DOI":"10.1109\/SP.2010.16"},{"issue":"4\u20135","key":"17_CR13","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. Program. 22(4\u20135), 477\u2013528 (2012)","journal-title":"J. Funct. Program."},{"key":"17_CR14","unstructured":"Skorstengaard, L., Devriese, D., Birkedal, L.: Reasoning about a machine with local capabilities: provably safe stack and return pointer management - technical appendix including proofs and details. Technical report, Department of Computer Science, Aarhus University (2018). https:\/\/cs.au.dk\/~birke\/papers\/local-capabilities-conf-tr.pdf"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","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: POPL, pp. 340\u2013353. ACM (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR16","unstructured":"Ahmed, A.J.: Semantics of types for mutable state. Ph.D. thesis, Princeton University (2004)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Thamsborg, J., Birkedal, L.: A Kripke logical relation for effect-based program transformations. In: ICFP, pp. 445\u2013456. ACM (2011)","DOI":"10.1145\/2034773.2034831"},{"key":"17_CR18","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: POPL, pp. 119\u2013132. ACM (2011)","DOI":"10.1145\/1925844.1926401"},{"key":"17_CR19","unstructured":"Birkedal, L., Bizjak, A.: A Taste of Categorical Logic Tutorial Notes (2014). http:\/\/cs.au.dk\/~birke\/modures\/tutorial\/categorical-logic-tutorial-notes.pdf"},{"key":"17_CR20","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"AM Pitts","year":"1998","unstructured":"Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 227\u2013274. Cambridge University Press, New York (1998)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-49255-0_70","volume-title":"Object-Oriented Technology: ECOOP\u201998 Workshop Reader","author":"M Abadi","year":"1998","unstructured":"Abadi, M.: Protection in programming-language translations: mobile object systems. In: Demeyer, S., Bosch, J. (eds.) ECOOP 1998. LNCS, vol. 1543, p. 291. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49255-0_70"},{"issue":"1","key":"17_CR22","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0168-0072(94)90047-7","volume":"68","author":"JL Krivine","year":"1994","unstructured":"Krivine, J.L.: Classical logic, storage operators and second-order lambda-calculus. Ann. Pure and Appl. Log. 68(1), 53\u201378 (1994)","journal-title":"Ann. Pure and Appl. Log."},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Dreyer, D.: A Kripke logical relation between ML and assembly. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 133\u2013146. ACM (2011)","DOI":"10.1145\/1926385.1926402"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Osvald, L., Essertel, G., Wu, X., Alay\u00f3n, L.I.G., Rompf, T.: Gentrification gone too far? Affordable 2nd-class values for fun and (co-)effect. In: Object-Oriented Programming, Systems, Languages, and Applications, pp. 234\u2013251. ACM (2016)","DOI":"10.1145\/3022671.2984009"},{"key":"17_CR25","volume-title":"Capability-Based Computer Systems","author":"HM Levy","year":"1984","unstructured":"Levy, H.M.: Capability-Based Computer Systems, vol. 12. Digital Press, Bedford (1984)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Patrignani, M., Devriese, D., Piessens, F.: On modular and fully-abstract compilation. In: Computer Security Foundations Symposium (CSF), pp. 17\u201330, June 2016","DOI":"10.1109\/CSF.2016.9"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Juglaret, Y., Hritcu, C., Amorim, A.A.D., Eng, B., Pierce, B.C.: Beyond good and evil: formalizing the security guarantees of compartmentalizing compilation. In: Computer Security Foundations Symposium (CSF), pp. 45\u201360, June 2016","DOI":"10.1109\/CSF.2016.11"},{"issue":"5","key":"17_CR28","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":"17_CR29","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.K.: Biorthogonality, step-indexing and compiler correctness. In: International Conference on Functional Programming, pp. 97\u2013108. ACM (2009)","DOI":"10.1145\/1596550.1596567"},{"issue":"OOPSLA","key":"17_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3133913","volume":"1","author":"David Swasey","year":"2017","unstructured":"Swasey, D., Garg, D., Dreyer, D.: Robust and compositional verification of object capability patterns (2017, to appear)","journal-title":"Proceedings of the ACM on Programming Languages"},{"issue":"1","key":"17_CR31","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/2775051.2676980","volume":"50","author":"Ralf Jung","year":"2015","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: POPL, pp. 637\u2013650 (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: ICFP, pp. 256\u2013269 (2016)","DOI":"10.1145\/2951913.2951943"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696\u2013723. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26"},{"issue":"1","key":"17_CR34","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/3093333.3009855","volume":"52","author":"Robbert Krebbers","year":"2017","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR35","unstructured":"El-Korashy, A.: A formal model for capability machines: an illustrative case study towards secure compilation to CHERI. Master\u2019s thesis, Saarland University, September 2016"}],"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-319-89884-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:03Z","timestamp":1571157183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}