{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:20:05Z","timestamp":1781893205006,"version":"3.54.5"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319071503","type":"print"},{"value":"9783319071510","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07151-0_16","type":"book-chapter","created":{"date-parts":[[2014,5,22]],"date-time":"2014-05-22T03:30:14Z","timestamp":1400729414000},"page":"253-269","source":"Crossref","is-referenced-by-count":4,"title":["Type Soundness and Race Freedom for Mezzo"],"prefix":"10.1007","author":[{"given":"Thibaut","family":"Balabonski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"4","key":"16_CR1","first-page":"397","volume":"77","author":"A. Ahmed","year":"2007","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L 3: A linear language with locations. Fundamenta Informatic\u00e6\u00a077(4), 397\u2013449 (2007)","journal-title":"Fundamenta Informatic\u00e6"},{"key":"16_CR2","unstructured":"Balabonski, T., Pottier, F.: A Coq formalization of Mezzo (December 2013), http:\/\/gallium.inria.fr\/~fpottier\/mezzo\/mezzo-coq.tar.gz"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.entcs.2011.09.018","volume":"276","author":"A. Buisse","year":"2011","unstructured":"Buisse, A., Birkedal, L., St\u00f8vring, K.: A step-indexed Kripke model of separation logic for storable locks. Electronic Notes in Theoretical Computer Science\u00a0276, 121\u2013143 (2011)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: International Conference on Functional Programming (ICFP), pp. 213\u2013224 (2008)","DOI":"10.1145\/1411203.1411235"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Certified Programming and Dependent Types. MIT Press (2013)","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Delaware, B., Oliveira, B.C.D.S., Schrijvers, T.: Meta-theory \u00e0 La Carte. In: Principles of Programming Languages (POPL), pp. 207\u2013218 (2013)","DOI":"10.1145\/2480359.2429094"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Principles of Programming Languages (POPL), pp. 287\u2013300 (2013)","DOI":"10.1145\/2480359.2429104"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. Tech. Rep. MSR-TR-2007-39, Microsoft Research (2007)","DOI":"10.1145\/1273920.1273941"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.jlap.2004.03.008","volume":"60","author":"P.D. Mosses","year":"2004","unstructured":"Mosses, P.D.: Modular structural operational semantics. Journal of Logic and Algebraic Programming\u00a060, 195\u2013228 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1-3","key":"16_CR10","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"16_CR11","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1017\/S0956796812000366","volume":"23","author":"F. Pottier","year":"2013","unstructured":"Pottier, F.: Syntactic soundness proof of a type-and-capability system with hidden state. Journal of Functional Programming\u00a023(1), 38\u2013144 (2013)","journal-title":"Journal of Functional Programming"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Pottier, F., Protzenko, J.: Programming with permissions in Mezzo. In: International Conference on Functional Programming (ICFP), pp. 173\u2013184 (2013)","DOI":"10.1145\/2544174.2500598"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science (LICS), pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"16_CR14","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: International Conference on Functional Programming (ICFP), pp. 377\u2013390 (2013)","DOI":"10.1145\/2544174.2500600"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07151-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:33:05Z","timestamp":1746232385000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-07151-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319071503","9783319071510"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07151-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}