{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:21Z","timestamp":1780994661146,"version":"3.54.1"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030449131","type":"print"},{"value":"9783030449148","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires <jats:italic>strong updates<\/jats:italic> to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_25","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"684-714","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs"],"prefix":"10.1007","author":[{"given":"John","family":"Toman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ren","family":"Siqi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"25_CR1","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L$$^3$$: a linear language with locations. Fundamenta Informaticae 77(4), 397\u2013449 (2007)"},{"key":"25_CR2","doi-asserted-by":"publisher","unstructured":"Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: Conference on Programming Language Design and Implementation (PLDI). pp. 129\u2013140 (2003). https:\/\/doi.org\/10.1145\/781131.781146","DOI":"10.1145\/781131.781146"},{"key":"25_CR3","doi-asserted-by":"publisher","unstructured":"Amtoft, T., Turbak, F.: Faithful translations between polyvariant flows and polymorphic types. In: European Symposium on Programming (ESOP). pp. 26\u201340. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_2","DOI":"10.1007\/3-540-46425-5_2"},{"key":"25_CR4","doi-asserted-by":"publisher","unstructured":"Bakst, A., Jhala, R.: Predicate abstraction for linked data structures. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 65\u201384. Springer, Berlin Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_3","DOI":"10.1007\/978-3-662-49122-5_3"},{"key":"25_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Communications of the ACM 54(7), 68\u201376 (2011). https:\/\/doi.org\/10.1145\/1965724.1965743","DOI":"10.1145\/1965724.1965743"},{"key":"25_CR6","doi-asserted-by":"publisher","unstructured":"Banerjee, A.: A modular, polyvariant and type-based closure analysis. In: International Conference on Functional Programming (ICFP), pp. 1\u201310 (1997). https:\/\/doi.org\/10.1145\/258948.258951","DOI":"10.1145\/258948.258951"},{"key":"25_CR7","doi-asserted-by":"publisher","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Communications of the ACM 54(6), 81\u201391 (2011). https:\/\/doi.org\/10.1145\/1953122.1953145","DOI":"10.1145\/1953122.1953145"},{"key":"25_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"25_CR9","doi-asserted-by":"publisher","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS) 33(2), 8:1\u2013845 (2011). https:\/\/doi.org\/10.1145\/1890028.1890031","DOI":"10.1145\/1890028.1890031"},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Bond, B., Delignat-Lavaud, A., Fournet, C., Hawblitzel, C., Hri\u0163cu, C., Ishtiaq, S., Kohlweiss, M., Leino, R., Lorch, J., Maillard, K., Pan, J., Parno, B., Protzenko, J., Ramananandro, T., Rane, A., Rastogi, A., Swamy, N., Thompson, L., Wang, P., Zanella-B\u00e9guelin, S., Zinzindohou\u00e9, J.K.: Everest: Towards a verified, drop-in replacement of HTTPS. In: Summit on Advances in Programming Languages (SNAPL 2017). pp. 1:1\u20131:12. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2017.1","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"25_CR11","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Symposium on Principles of Programming Languages (POPL). pp. 259\u2013270 (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"25_CR12","doi-asserted-by":"publisher","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Symposion on Static Analysis (SAS). pp. 55\u201372. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44898-54","DOI":"10.1007\/3-540-44898-54"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"Champion, A., Kobayashi, N., Sato, R.: HoIce: An ICE-based non-linear Horn clause solver. In: Asian Symposium on Programming Languages and Systems (APLAS). pp. 146\u2013156. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-18","DOI":"10.1007\/978-3-030-02768-18"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). pp. 587\u2013606 (2012). https:\/\/doi.org\/10.1145\/2384616.2384659","DOI":"10.1145\/2384616.2384659"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyzer. In: European Symposium on Programming (ESOP). pp. 21\u201330. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-03","DOI":"10.1007\/978-3-540-31987-03"},{"key":"25_CR16","doi-asserted-by":"publisher","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-324","DOI":"10.1007\/978-3-540-78800-324"},{"key":"25_CR17","doi-asserted-by":"publisher","unstructured":"Degen, M., Thiemann, P., Wehr, S.: Tracking linear and affine resources with JAVA(X). In: European Conference on Object-Oriented Programming (ECOOP). pp. 550\u2013574. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73589-2_26","DOI":"10.1007\/978-3-540-73589-2_26"},{"key":"25_CR18","doi-asserted-by":"publisher","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Conference on Programming Language Design and Implementation (PLDI), pp. 59\u201369 (2001). https:\/\/doi.org\/10.1145\/378795.378811","DOI":"10.1145\/378795.378811"},{"key":"25_CR19","doi-asserted-by":"publisher","unstructured":"F\u00e4hndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: Conference on Programming Language Design and Implementation (PLDI), pp. 13\u201324 (2002). https:\/\/doi.org\/10.1145\/512529.512532","DOI":"10.1145\/512529.512532"},{"key":"25_CR20","doi-asserted-by":"publisher","unstructured":"Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Transactions on Software Engineering and Methodology (TOSEM) 17(2), 91\u2013934 (2008). https:\/\/doi.org\/10.1145\/1348250.1348255","DOI":"10.1145\/1348250.1348255"},{"key":"25_CR21","doi-asserted-by":"publisher","unstructured":"Flanagan, C.: Hybrid type checking. In: Symposium on Principles of Programming Languages (POPL). pp. 245\u2013256 (2006). https:\/\/doi.org\/10.1145\/1111037.1111059","DOI":"10.1145\/1111037.1111059"},{"key":"25_CR22","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Conference on Programming Language Design and Implementation (PLDI). pp. 234\u2013245 (2002). https:\/\/doi.org\/10.1145\/512529.512558","DOI":"10.1145\/512529.512558"},{"key":"25_CR23","doi-asserted-by":"publisher","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Conference on Programming Language Design and Implementation (PLDI). pp. 1\u201312 (2002). https:\/\/doi.org\/10.1145\/512529.512531","DOI":"10.1145\/512529.512531"},{"key":"25_CR24","doi-asserted-by":"publisher","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. In: Conference on Programming Language Design and Implementation (PLDI). pp. 268\u2013277 (1991). https:\/\/doi.org\/10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"25_CR25","doi-asserted-by":"publisher","unstructured":"Gilray, T., Might, M.: A survey of polyvariance in abstract interpretations. In: Symposium on Trends in Functional Programming. pp. 134\u2013148. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-45340-3_9","DOI":"10.1007\/978-3-642-45340-3_9"},{"key":"25_CR26","doi-asserted-by":"publisher","unstructured":"Gordon, C.S., Ernst, M.D., Grossman, D.: Rely-guarantee references for refinement types over aliased mutable data. In: Conference on Programming Language Design and Implementation (PLDI). pp. 73\u201384 (2013). https:\/\/doi.org\/10.1145\/2491956.2462160","DOI":"10.1145\/2491956.2462160"},{"key":"25_CR27","doi-asserted-by":"publisher","unstructured":"Gordon, C.S., Ernst, M.D., Grossman, D., Parkinson, M.J.: Verifying invariants of lock-free data structures with rely-guarantee and refinement types. ACM Transactions on Programming Languages and Systems (TOPLAS) bf 39(3), 11:1\u201311:54 (2017). https:\/\/doi.org\/10.1145\/3064850","DOI":"10.1145\/3064850"},{"key":"25_CR28","doi-asserted-by":"publisher","unstructured":"Hardekopf, B., Wiedermann, B., Churchill, B., Kashyap, V.: Widening for control-flow. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 472\u2013491 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_26","DOI":"10.1007\/978-3-642-54013-4_26"},{"key":"25_CR29","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In: Symposium on Operating Systems Principles (SOSP). pp. 1\u201317. ACM (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"25_CR30","doi-asserted-by":"publisher","unstructured":"Heule, S., Kassios, I.T., M\u00fcller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: European Conference on Object-Oriented Programming (ECOOP). pp. 451\u2013476. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39038-8_19","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"25_CR31","doi-asserted-by":"publisher","unstructured":"Heule, S., Leino, K.R.M., M\u00fcller, P., Summers, A.J.: Abstract read permissions: Fractional permissions without the fractions. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 315\u2013334 (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_20","DOI":"10.1007\/978-3-642-35873-9_20"},{"key":"25_CR32","unstructured":"Kahsai, T., Kersten, R., R\u00fcmmer, P., Sch\u00e4f, M.: Quantified heap invariants for object-oriented programs. In: Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 368\u2013384 (2017)"},{"key":"25_CR33","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: A framework for verifying Java programs. In: Conference on Computer Aided Verification (CAV). pp. 352\u2013358. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"25_CR34","doi-asserted-by":"publisher","unstructured":"Kashyap, V., Dewey, K., Kuefner, E.A., Wagner, J., Gibbons, K., Sarracino, J., Wiedermann, B., Hardekopf, B.: JSAI: a static analysis platform for JavaScript. In: Conference on Foundations of Software Engineering (FSE). pp. 121\u2013132 (2014). https:\/\/doi.org\/10.1145\/2635868.2635904","DOI":"10.1145\/2635868.2635904"},{"key":"25_CR35","doi-asserted-by":"publisher","unstructured":"Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: Conference on Programming Language Design and Implementation (PLDI). pp. 304\u2013315 (2009). https:\/\/doi.org\/10.1145\/1542476.1542510","DOI":"10.1145\/1542476.1542510"},{"key":"25_CR36","doi-asserted-by":"publisher","unstructured":"Kloos, J., Majumdar, R., Vafeiadis, V.: Asynchronous liquid separation types. In: European Conference on Object-Oriented Programming (ECOOP). pp. 396\u2013420. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.396","DOI":"10.4230\/LIPIcs.ECOOP.2015.396"},{"key":"25_CR37","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Conference on Computer Aided Verification (CAV). pp. 846\u2013862. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"25_CR38","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"25_CR39","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Deadlock-free channels and locks. In: European Symposium on Programming (ESOP). pp. 407\u2013426. Springer-Verlag (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_22","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"25_CR40","doi-asserted-by":"crossref","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. In: European Symposium on Programming (ESOP). Springer (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25d55"},{"key":"25_CR41","doi-asserted-by":"publisher","unstructured":"Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering and Methodology (TOSEM) 14(1), 1\u201341 (2005). https:\/\/doi.org\/10.1145\/1044834.1044835","DOI":"10.1145\/1044834.1044835"},{"key":"25_CR42","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 41\u201362. Springer-Verlag (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"25_CR43","unstructured":"Pierce, B.C.: Types and programming languages. MIT press (2002)"},{"key":"25_CR44","doi-asserted-by":"publisher","unstructured":"Protzenko, J., Zinzindohou\u00e9, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-B\u00e9guelin, S., Delignat-Lavaud, A., Hri\u0163cu, C., Bhargavan, K., Fournet, C., Swamy, N.: Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages 1(ICFP), 17:1\u201317:29 (2017). https:\/\/doi.org\/10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"25_CR45","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS). pp. 55\u201374. IEEE (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"25_CR46","doi-asserted-by":"publisher","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: Symposium on Principles of Programming Languages (POPL). pp. 131\u2013144 (2010). https:\/\/doi.org\/10.1145\/1706299.1706316","DOI":"10.1145\/1706299.1706316"},{"key":"25_CR47","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Conference on Programming Language Design and Implementation (PLDI). pp. 159\u2013169 (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"25_CR48","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Conference on Computer Aided Verification (CAV). pp. 347\u2013363. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_24","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"25_CR49","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, chap. 7, pp. 189\u2013223. Prentice Hall (1981)"},{"key":"25_CR50","unstructured":"Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University (1991)"},{"key":"25_CR51","doi-asserted-by":"publisher","unstructured":"Smaragdakis, Y., Bravenboer, M., Lhot\u00e1k, O.: Pick your contexts well: Understanding object-sensitivity. In: Symposium on Principles of Programming Languages (POPL). pp. 17\u201330 (2011). https:\/\/doi.org\/10.1145\/1926385.1926390","DOI":"10.1145\/1926385.1926390"},{"key":"25_CR52","doi-asserted-by":"publisher","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: European Symposium on Programming (ESOP). pp. 366\u2013381. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_24","DOI":"10.1007\/3-540-46425-5_24"},{"key":"25_CR53","doi-asserted-by":"publisher","unstructured":"Sp\u00e4th, J., Ali, K., Bodden, E.: Context-, flow-, and field-sensitive data-flow analysis using synchronized pushdown systems. Proceedings of the ACM on Programming Languages 3(POPL), 48:1\u201348:29 (2019). https:\/\/doi.org\/10.1145\/3290361","DOI":"10.1145\/3290361"},{"key":"25_CR54","doi-asserted-by":"publisher","unstructured":"Sp\u00e4th, J., Nguyen Quang Do, L., Ali, K., Bodden, E.: Boomerang: Demand-driven flow-and context-sensitive pointer analysis for Java. In: European Conference on Object-Oriented Programming (ECOOP). pp. 22:1\u201322:26. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2016.22","DOI":"10.4230\/LIPIcs.ECOOP.2016.22"},{"key":"25_CR55","doi-asserted-by":"publisher","unstructured":"Suenaga, K., Fukuda, R., Igarashi, A.: Type-based safe resource deallocation for shared-memory concurrency. In: Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). pp. 1\u201320 (2012). https:\/\/doi.org\/10.1145\/2384616.2384618","DOI":"10.1145\/2384616.2384618"},{"key":"25_CR56","doi-asserted-by":"publisher","unstructured":"Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory deallocation. In: Asian Symposium on Programming Languages and Systems (APLAS). pp. 128\u2013143. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_11","DOI":"10.1007\/978-3-642-10672-9_11"},{"key":"25_CR57","doi-asserted-by":"publisher","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohou\u00e9, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: Symposium on Principles of Programming Languages (POPL). pp. 256\u2013270 (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"25_CR58","doi-asserted-by":"publisher","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Conference on Programming Language Design and Implementation (PLDI). pp. 387\u2013398 (2013). https:\/\/doi.org\/10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"25_CR59","doi-asserted-by":"publisher","unstructured":"Terauchi, T.: Checking race freedom via linear programming. In: Conference on Programming Language Design and Implementation (PLDI). pp. 1\u201310 (2008). https:\/\/doi.org\/10.1145\/1375581.1375583","DOI":"10.1145\/1375581.1375583"},{"key":"25_CR60","doi-asserted-by":"crossref","unstructured":"Toman, J., Siqi, R., Suenaga, K., Igarashi, A., Kobayashi, N.: Consort: Context- and flow-sensitive ownership refinement types for imperative programs. https:\/\/arxiv.org\/abs\/2002.07770 (2020)","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"25_CR61","doi-asserted-by":"publisher","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Conference on Principles and Practice of Declarative Programming (PPDP). pp. 277\u2013288. ACM (2009). https:\/\/doi.org\/10.1145\/1599410.1599445","DOI":"10.1145\/1599410.1599445"},{"key":"25_CR62","doi-asserted-by":"publisher","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: European Symposium on Programming (ESOP). pp. 209\u2013228. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"25_CR63","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: International Conference on Functional Programming (ICFP). pp. 269\u2013282 (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"25_CR64","doi-asserted-by":"publisher","unstructured":"Wells, J.B., Dimock, A., Muller, R., Turbak, F.: A calculus with polymorphic and polyvariant flow types. Journal of Functional Programming 12(3), 183\u2013227 (2002). https:\/\/doi.org\/10.1017\/S0956796801004245","DOI":"10.1017\/S0956796801004245"},{"key":"25_CR65","doi-asserted-by":"publisher","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Symposium on Principles of Programming Languages (POPL). pp. 214\u2013227. ACM (1999). https:\/\/doi.org\/10.1145\/292540.292560","DOI":"10.1145\/292540.292560"},{"key":"25_CR66","doi-asserted-by":"publisher","unstructured":"Zave, P.: Using lightweight modeling to understand Chord. ACM SIGCOMM Computer Communication Review 42(2), 49\u201357 (2012). https:\/\/doi.org\/10.1145\/2185376.2185383","DOI":"10.1145\/2185376.2185383"},{"key":"25_CR67","doi-asserted-by":"publisher","unstructured":"Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 295\u2013314. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_19","DOI":"10.1007\/978-3-642-35873-9_19"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:12:51Z","timestamp":1656609171000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}