{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:46Z","timestamp":1779836746429,"version":"3.53.1"},"reference-count":89,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2012,10,10]],"date-time":"2012-10-10T00:00:00Z","timestamp":1349827200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper presents a formal definition and machine-checked soundness proof for a very expressive type-and-capability system, that is, a low-level type system that keeps precise track of ownership and side effects. The programming language has first-class functions and references. The type system's features include the following: universal, existential, and recursive types; subtyping; a distinction between affine and unrestricted data; support for strong updates; support for naming values and heap fragments via singleton and group regions; a distinction between ordinary values (which exist at runtime) and capabilities (which do not); support for dynamic reorganizations of the ownership hierarchy by disassembling and reassembling capabilities; and support for temporarily or permanently hiding a capability via frame and anti-frame rules. One contribution of the paper is the definition of the type-and-capability system itself. We present the system as modularly as possible. In particular, at the core of the system, the treatment of affinity, in the style of dual intuitionistic linear logic, is formulated in terms of an arbitrary\n                    <jats:italic>monotonic separation algebra<\/jats:italic>\n                    , a novel axiomatization of resources, ownership, and the manner in which they evolve with time. Only the peripheral layers of the system are aware that we are dealing with a specific monotonic separation algebra, whose resources are references and regions. This semi-abstract organization should facilitate further extensions of the system with new forms of resources. The other main contribution is a machine-checked proof of type soundness. The proof is carried out in the Wright and Felleisen's syntactic style. This offers an evidence that this relatively simple-minded proof technique can scale up to systems of this complexity, and constitutes a viable alternative to more sophisticated semantic proof techniques. We do not claim that the syntactic technique is superior: We simply illustrate how it is used and highlight its strengths and shortcomings.\n                  <\/jats:p>","DOI":"10.1017\/s0956796812000366","type":"journal-article","created":{"date-parts":[[2012,10,10]],"date-time":"2012-10-10T19:26:44Z","timestamp":1349897204000},"page":"38-144","source":"Crossref","is-referenced-by-count":14,"title":["Syntactic soundness proof of a type-and-capability system with hidden state"],"prefix":"10.1017","volume":"23","author":[{"given":"FRAN\u00c7OIS","family":"POTTIER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,10,10]]},"reference":[{"key":"S0956796812000366_ref46","first-page":"353","volume-title":"European Symposium on Programming (ESOP)","author":"Hobor","year":"2008"},{"key":"S0956796812000366_ref39","unstructured":"Gauthier N. & Pottier F. (2004) Numbering matters: First-order canonical forms for second-order recursive types. In Proceedings of the ACM International Conference on Functional Programming (ICFP), pp. 150\u2013161."},{"key":"S0956796812000366_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"S0956796812000366_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749611"},{"key":"S0956796812000366_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"S0956796812000366_ref33","unstructured":"Dinsdale-Young T. , Birkedal L. , Gardner P. , Parkinson M. J. & Yang H. (submitted) Views: Compositional Reasoning for Concurrent Programs."},{"key":"S0956796812000366_ref26","doi-asserted-by":"crossref","unstructured":"Clarke D. G. , Potter J. M. & Noble J. (1998) Ownership types for flexible alias protection. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 48\u201364.","DOI":"10.1145\/286936.286947"},{"key":"S0956796812000366_ref42","first-page":"147","volume-title":"European Symposium on Programming (ESOP)","author":"Glew","year":"2002"},{"key":"S0956796812000366_ref30","unstructured":"DeLine R. & F\u00e4hndrich M. (2001) Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation (PLDI), pp. 59\u201369."},{"key":"S0956796812000366_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796812000366_ref87","first-page":"177","volume-title":"Workshop on Types in Compilation (TIC)","author":"Walker","year":"2000"},{"key":"S0956796812000366_ref23","doi-asserted-by":"crossref","unstructured":"Calcagno C. , O'Hearn P. W. & Yang H. (2007) Local action and abstract separation logic. In IEEE Symposium on Logic in Computer Science (LICS), pp. 366\u2013378.","DOI":"10.1109\/LICS.2007.30"},{"key":"S0956796812000366_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"S0956796812000366_ref37","unstructured":"F\u00e4hndrich M. & DeLine R. (2002) Adoption and focus: Practical linear types for imperative programming. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), pp. 13\u201324."},{"key":"S0956796812000366_ref61","unstructured":"Peyton Jones, S. & Wadler P. (1993) Imperative functional programming. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pp. 71\u201384."},{"key":"S0956796812000366_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0956796812000366_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000120"},{"key":"S0956796812000366_ref5","first-page":"397","article-title":"L3: A linear language with locations","volume":"77","author":"Ahmed","year":"2007","journal-title":"Fundam. Inform."},{"key":"S0956796812000366_ref4","doi-asserted-by":"crossref","unstructured":"Ahmed Amal J. , Fluet M. & Morrisett G. (2005) A step-indexed model of substructural state. In ACM International Conference on Functional Programming (ICFP), pp. 78\u201391.","DOI":"10.1145\/1086365.1086376"},{"key":"S0956796812000366_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_8"},{"key":"S0956796812000366_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000162"},{"key":"S0956796812000366_ref31","volume-title":"Wrestling with Rep Exposure","author":"Detlefs","year":"1998"},{"key":"S0956796812000366_ref14","first-page":"456","volume-title":"International Conference on Foundations of Software Science and Computation Structures (FOSSACS)","author":"Birkedal","year":"2009"},{"key":"S0956796812000366_ref20","unstructured":"Boyland J. T. & Retert W. (2005) Connecting effects and uniqueness with adoption. In ACM Symposium on Principles of Programming Languages (POPL), pp. 283\u2013295."},{"key":"S0956796812000366_ref40","doi-asserted-by":"publisher","DOI":"10.21236\/ADA256798"},{"key":"S0956796812000366_ref59","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"S0956796812000366_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"S0956796812000366_ref81","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"S0956796812000366_ref2","unstructured":"Ahmed A. J. (2004) Semantics of Types for Mutable State. Ph.D. thesis, Princeton University, Princeton, NJ."},{"key":"S0956796812000366_ref1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054191000029"},{"key":"S0956796812000366_ref32","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"S0956796812000366_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"S0956796812000366_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"S0956796812000366_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"S0956796812000366_ref27","doi-asserted-by":"crossref","unstructured":"Crary K. , Walker D. & Morrisett G. (1999) Typed memory management in a calculus of capabilities. In ACM Symposium on Principles of Programming Languages (POPL), pp. 262\u2013275.","DOI":"10.1145\/292540.292564"},{"key":"S0956796812000366_ref8","first-page":"85","volume-title":"European Symposium on Programming (ESOP)","author":"Atkey","year":"2010"},{"key":"S0956796812000366_ref62","volume-title":"Workshop on Types in Language Design and Implementation (TLDI)","author":"Pilkiewicz","year":"2011"},{"key":"S0956796812000366_ref25","unstructured":"Chargu\u00e9raud A. & Pottier F. (2008) Functional translation of a calculus of capabilities. In ACM International Conference on Functional Programming (ICFP), pp. 213\u2013224."},{"key":"S0956796812000366_ref11","volume-title":"Proceedings of the International Workshop on Proof-Carrying Code (PCC)","author":"Bell","year":"2008"},{"key":"S0956796812000366_ref12","unstructured":"Bierhoff K. & Aldrich J. (2007) Modular typestate checking of aliased objects. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 301\u2013320."},{"key":"S0956796812000366_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"S0956796812000366_ref16","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"S0956796812000366_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"S0956796812000366_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"S0956796812000366_ref78","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.02.003"},{"key":"S0956796812000366_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S0956796812000366_ref56","volume-title":"Universes: A Type System for Alias and Dependency Control","author":"M\u00fcller","year":"2001"},{"key":"S0956796812000366_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.018"},{"key":"S0956796812000366_ref36","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich M. , Aiken M. , Hawblitzel C. , Hodson O. , Hunt G. , Larus J. R. & Levi S. (2006) Language support for fast and reliable message-based communication in Singularity OS. In Proceedings of the EuroSys, pp. 177\u2013190.","DOI":"10.1145\/1217935.1217953"},{"key":"S0956796812000366_ref47","first-page":"258","article-title":"A type system for bounded space and functional in-place update","volume":"7","author":"Hofmann","year":"2000","journal-title":"Nord. J. Comput."},{"key":"S0956796812000366_ref49","unstructured":"Ishtiaq Samin S. & O'Hearn Peter W. (2001) BI as an assertion language for mutable data structures. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pp. 14\u201326."},{"key":"S0956796812000366_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"S0956796812000366_ref84","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"S0956796812000366_ref51","volume-title":"Computer Science Logic","author":"Levy","year":"2002"},{"key":"S0956796812000366_ref89","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796812000366_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"S0956796812000366_ref18","doi-asserted-by":"crossref","unstructured":"Boyapati C. , Lee R. & Rinard M. (2002) Ownership types for safe programming: Preventing data races and deadlocks. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 211\u2013230.","DOI":"10.1145\/582419.582440"},{"key":"S0956796812000366_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"S0956796812000366_ref6","first-page":"32","volume-title":"European Conference on Object-Oriented Programming","author":"Almeida","year":"1997"},{"key":"S0956796812000366_ref75","first-page":"305","volume-title":"International Conference on Foundations of Software Science and Computation Structures (FOSSACS)","author":"Schwinghammer","year":"2011"},{"key":"S0956796812000366_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"S0956796812000366_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9229-y"},{"key":"S0956796812000366_ref64","doi-asserted-by":"crossref","unstructured":"Pottier F. (2008) Hiding local state in direct style: A higher-order anti-frame rule. In IEEE Symposium on Logic in Computer Science (LICS), pp. 331\u2013340.","DOI":"10.1109\/LICS.2008.16"},{"key":"S0956796812000366_ref10","volume-title":"Dual Intuitionistic Linear Logic","author":"Barber","year":"1996"},{"key":"S0956796812000366_ref65","unstructured":"Pottier F. (2009a) Generalizing the higher-order frame and anti-frame rules. Unpublished manuscript."},{"key":"S0956796812000366_ref55","unstructured":"Monnier S. (2008) Statically Tracking State with Typed Regions. Draft."},{"key":"S0956796812000366_ref66","unstructured":"Pottier F. (2009b). Three comments on the anti-frame rule. Unpublished manuscript."},{"key":"S0956796812000366_ref68","unstructured":"Pottier F. (2012b) Accompanying Coq scripts; for downloading [online]. Available at: http:\/\/gallium.inria.fr\/~fpottier\/ssphs\/ssphs.tar.gz and also as an online supplement at http:\/\/www.cambridge.org\/.\u00a0.\u00a0.\u00a0. Accessed 21 September 2012."},{"key":"S0956796812000366_ref69","doi-asserted-by":"crossref","unstructured":"Pottier F. & Protzenko J. (2012) Programming with permissions: An introduction to Mezzo. Unpublished manuscript.","DOI":"10.1145\/2500365.2500598"},{"key":"S0956796812000366_ref71","first-page":"408","volume-title":"Colloque sur la Programmation","author":"Reynolds","year":"1974"},{"key":"S0956796812000366_ref67","unstructured":"Pottier F. (2012a) Accompanying Coq scripts; for browsing [online]. Available at: http:\/\/gallium.inria.fr\/~fpottier\/ssphs\/. Accessed 21 September 2012."},{"key":"S0956796812000366_ref72","doi-asserted-by":"crossref","unstructured":"Reynolds John C. (2002) Separation logic: A logic for shared mutable data structures. In IEEE Symposium on Logic in Computer Science (LICS), pp. 55\u201374.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"S0956796812000366_ref82","first-page":"550","volume-title":"European Symposium on Programming (ESOP)","author":"Tov","year":"2010"},{"key":"S0956796812000366_ref88","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"S0956796812000366_ref21","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","article-title":"Coinductive axiomatization of recursive type equality and subtyping.","volume":"33","author":"Brandt","year":"1998","journal-title":"Fundam. Inform."},{"key":"S0956796812000366_ref73","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000035"},{"key":"S0956796812000366_ref57","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"S0956796812000366_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_32"},{"key":"S0956796812000366_ref41","first-page":"7","volume-title":"Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de L'arithm\u00e9tique D'ordre Sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"S0956796812000366_ref77","first-page":"366","volume-title":"European Symposium on Programming (ESOP)","author":"Smith","year":"2000"},{"key":"S0956796812000366_ref79","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"S0956796812000366_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_14"},{"key":"S0956796812000366_ref83","unstructured":"Tov J. A. & Pucella R. (2011) Practical affine types. In ACM Symposium on Principles of Programming Languages (POPL), pp. 447\u2013458."},{"key":"S0956796812000366_ref85","unstructured":"Vouillon J. & Melli\u00e8s P.-A. (2004) Semantic types: A fresh look at the ideal model for types. In ACM Symposium on Principles of Programming Languages (POPL), pp. 52\u201363."},{"key":"S0956796812000366_ref76","first-page":"2","volume-title":"International Conference on Foundations of Software Science and Computation Structures (FOSSACS)","author":"Schwinghammer","year":"2010"},{"key":"S0956796812000366_ref86","first-page":"3","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker","year":"2005"},{"key":"S0956796812000366_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"S0956796812000366_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_38"},{"key":"S0956796812000366_ref60","doi-asserted-by":"crossref","unstructured":"O'Hearn P. W. , Yang H. & Reynolds J. C. (2004) Separation and information hiding. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pp. 268\u2013280.","DOI":"10.1145\/964001.964024"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:26Z","timestamp":1779834986000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000366\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,10]]},"references-count":89,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["S0956796812000366"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000366","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,10]]}}}