{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:29Z","timestamp":1750308089323,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2005,1]]},"abstract":"<jats:p>\n            Read-only fields are useful in object calculi, pi calculi, and statically typed intermediate languages because they admit covariant subtyping, unlike updateable fields. For example, Glew's translation of classes and objects to an intermediate calculus relies crucially on covariant subtyping of read-only fields to ensure that subclasses are translated to subtypes.In this article, we present a type inference algorithm for an Abadi--Cardelli object calculus in which fields are marked either as updateable or as read-only. The type inference problem is P-complete, and our algorithm runs in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            ) time. The same complexity results hold for the calculus in which the fields are not explicitly annotated as updateable or read-only; perhaps surprisingly, the annotations do not make type inference easier. We show that type inference is equivalent to the problem of solving type constraints, and this forms the core of our algorithm and implementation.\n          <\/jats:p>","DOI":"10.1145\/1053468.1053472","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"126-162","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Automatic discovery of covariant read-only fields"],"prefix":"10.1145","volume":"27","author":[{"given":"Jens","family":"Palsberg","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, IN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tian","family":"Zhao","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, IN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Trevor","family":"Jim","sequence":"additional","affiliation":[{"name":"AT&amp;T Labs Research, Florham Park, NJ"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,1]]},"reference":[{"volume-title":"1996. A Theory of Objects","author":"Abadi M.","key":"e_1_2_1_1_1","unstructured":"Abadi , M. and Cardelli , L . 1996. A Theory of Objects . Springer-Verlag , New York . Abadi, M. and Cardelli, L.1996. A Theory of Objects. Springer-Verlag, New York."},{"key":"e_1_2_1_2_1","first-page":"31","volume-title":"Proceedings of Conference on Functional Programming Languages and Computer Architecture.","author":"Aiken A.","unstructured":"Aiken , A. and Wimmers , E . 1993. Type inclusion constraints and type inference . In Proceedings of Conference on Functional Programming Languages and Computer Architecture. pp. 31 -- 41 . 10.1145\/165180.165188 Aiken, A. and Wimmers, E.1993. Type inclusion constraints and type inference. In Proceedings of Conference on Functional Programming Languages and Computer Architecture. pp. 31--41. 10.1145\/165180.165188"},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Mathematical Foundations of Computer Science","author":"Benke M.","unstructured":"Benke , M. 1993. Efficient type reconstruction in the presence of inheritance . In Proceedings of Mathematical Foundations of Computer Science . Lecture Notes in Computer Science , vol. 711 . Springer-Verlag , New York , 272--280. Benke, M.1993. Efficient type reconstruction in the presence of inheritance. In Proceedings of Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, New York, 272--280."},{"key":"e_1_2_1_4_1","first-page":"183","volume-title":"Proceedings of OOPSLA'98","author":"Bracha G.","unstructured":"Bracha , G. , Odersky , M. , Stoutamire , D. , and Wadler , P . 1998. Making the future safe for the past: Adding genericity to the Java programming language . In Proceedings of OOPSLA'98 , ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. ACM, New York , pp. 183 -- 200 . 10.1145\/286936.286957 Bracha, G., Odersky, M., Stoutamire, D., and Wadler, P.1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of OOPSLA'98, ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. ACM, New York, pp. 183--200. 10.1145\/286936.286957"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3091"},{"key":"e_1_2_1_6_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of SAS'97, International Static Analysis Symposium","author":"Frey A.","unstructured":"Frey , A. 1997. Satisfying systems of subtype inequalities in polynomial space . In Proceedings of SAS'97, International Static Analysis Symposium . Lecture Notes in Computer Science . Springer-Verlag , New York . Frey, A.1997. Satisfying systems of subtype inequalities in polynomial space. In Proceedings of SAS'97, International Static Analysis Symposium. Lecture Notes in Computer Science. Springer-Verlag, New York."},{"key":"e_1_2_1_7_1","first-page":"311","volume-title":"Proceedings of OOPSLA'00","author":"Glew N.","unstructured":"Glew , N. 2000. An efficient class and object encoding . In Proceedings of OOPSLA'00 , ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (Minneapolis, Minn. Oct.). ACM, New York , pp. 311 -- 324 . 10.1145\/353171.353192 Glew, N.2000. An efficient class and object encoding. In Proceedings of OOPSLA'00, ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (Minneapolis, Minn. Oct.). ACM, New York, pp. 311--324. 10.1145\/353171.353192"},{"volume-title":"Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages. http:\/\/www.cs.williams.edu\/kim\/FOOL\/index.html.","author":"Henglein F.","key":"e_1_2_1_8_1","unstructured":"Henglein , F. 1997. Breaking through the n3 barrier: Faster object type inference . In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages. http:\/\/www.cs.williams.edu\/kim\/FOOL\/index.html. Henglein, F.1997. Breaking through the n3 barrier: Faster object type inference. In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages. http:\/\/www.cs.williams.edu\/kim\/FOOL\/index.html."},{"key":"e_1_2_1_9_1","first-page":"176","volume-title":"Proceedings of POPL'95","author":"Hoang M.","year":"1994","unstructured":"Hoang , M. and Mitchell , J. C . 1995. Lower bounds on type inference with subtypes . In Proceedings of POPL'95 , 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages. ACM, New York , pp. 176 -- 185 . 10.1145\/ 1994 48.199481 Hoang, M. and Mitchell, J. C.1995. Lower bounds on type inference with subtypes. In Proceedings of POPL'95, 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages. ACM, New York, pp. 176--185. 10.1145\/199448.199481"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2872"},{"volume-title":"Proceedings of ECOOP'02","author":"Igarashi A.","key":"e_1_2_1_11_1","unstructured":"Igarashi , A. and Viroli , M . 2002. On variance-based subtyping for parametric types . In Proceedings of ECOOP'02 , 16th European Conference on Object-Oriented Programming. Igarashi, A. and Viroli, M.2002. On variance-based subtyping for parametric types. In Proceedings of ECOOP'02, 16th European Conference on Object-Oriented Programming."},{"key":"e_1_2_1_12_1","first-page":"363 80051","volume-title":"33rd IEEE Symposium on Foundations of Computer Science","author":"Kozen D.","unstructured":"Kozen , D. , Palsberg , J. , and Schwartzbach , M. I . 1994. Efficient inference of partial types. J. Comput. Syst. Sci. 49, 2, 306--324. Preliminary version in Proceedings of FOCS'92 , 33rd IEEE Symposium on Foundations of Computer Science ( Pittsburgh, Pa., Oct.). IEEE Computer Society Press, Los Alamitos, Calif. , pp. 363 -- 371 . 10.1016\/S0022-0000(05) 80051 - 80050 Kozen, D., Palsberg, J., and Schwartzbach, M. I.1994. Efficient inference of partial types. J. Comput. Syst. Sci. 49, 2, 306--324. Preliminary version in Proceedings of FOCS'92, 33rd IEEE Symposium on Foundations of Computer Science (Pittsburgh, Pa., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 363--371. 10.1016\/S0022-0000(05)80051-0"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581774"},{"key":"e_1_2_1_15_1","first-page":"1201","volume-title":"Handbook of Theoretical Computer Science","author":"Milner R.","unstructured":"Milner , R. 1990. Operational and algebraic semantics of concurrent processes . In Handbook of Theoretical Computer Science , vol. B: Formal Models and Semantics, Chap. 19 , J. van Leewen, Ed. The MIT Press , New York, N.Y., pp. 1201 -- 1242 . Milner, R.1990. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Chap. 19, J. van Leewen, Ed. The MIT Press, New York, N.Y., pp. 1201--1242."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90033-X"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1017\/S0956796800000113","article-title":"Type inference with simple subtypes","volume":"1","author":"Mitchell J. C.","year":"1991","unstructured":"Mitchell , J. C. 1991 . Type inference with simple subtypes . J. Funct. Prog. 1 , 245 -- 285 . Mitchell, J. C.1991. Type inference with simple subtypes. J. Funct. Prog. 1, 245--285.","journal-title":"J. Funct. Prog."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009866317252"},{"key":"e_1_2_1_19_1","first-page":"357","volume-title":"Proceedings of PARLE'89","author":"Nielson F.","unstructured":"Nielson , F. 1989. The typed lambda-calculus with first-class processes . In Proceedings of PARLE'89 . pp. 357 -- 373 . Nielson, F.1989. The typed lambda-calculus with first-class processes. In Proceedings of PARLE'89. pp. 357--373."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1109\/LICS.1994.316073","volume-title":"Ninth Annual IEEE Symposium on Logic in Computer Science","author":"Palsberg J.","year":"1994","unstructured":"Palsberg , J. 1995. Efficient inference of object types. Inf. Comput. 123, 2, 198--209. (Preliminary version in Proceedings of LICS'94 , Ninth Annual IEEE Symposium on Logic in Computer Science ( Paris, France , July 1994 ), pp. 186 -- 195 .) 10.1006\/inco.1995.1168 Palsberg, J.1995. Efficient inference of object types. Inf. Comput. 123, 2, 198--209. (Preliminary version in Proceedings of LICS'94, Ninth Annual IEEE Symposium on Logic in Computer Science (Paris, France, July 1994), pp. 186--195.) 10.1006\/inco.1995.1168"},{"key":"e_1_2_1_21_1","first-page":"259","article-title":"Type inference with simple selftypes is NP-complete","volume":"4","author":"Palsberg J.","year":"1997","unstructured":"Palsberg , J. and Jim , T. 1997 . Type inference with simple selftypes is NP-complete . Nord. J. Comput. 4 , 3, 259 -- 286 . Palsberg, J. and Jim, T.1997. Type inference with simple selftypes is NP-complete. Nord. J. Comput. 4, 3, 259--286.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_22_1","first-page":"367","volume-title":"22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"Palsberg J.","year":"1995","unstructured":"Palsberg , J. and O'Keefe , P. M. 1995. A type system equivalent to flow analysis. ACM Trans. Prog. Lang. Syst. 17, 4 (July), 576--599. (Preliminary version in Proceedings of POPL'95 , 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages ( San Francisco, Calif. , Jan. 1995 ), pp. 367 -- 378 .) 10.1145\/199448.199533 Palsberg, J. and O'Keefe, P. M.1995. A type system equivalent to flow analysis. ACM Trans. Prog. Lang. Syst. 17, 4 (July), 576--599. (Preliminary version in Proceedings of POPL'95, 22nd Annual SIGPLAN--SIGACT Symposium on Principles of Programming Languages (San Francisco, Calif., Jan. 1995), pp. 367--378.) 10.1145\/199448.199533"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/232706.232715"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/BF01212524","article-title":"Type inference with non-structural subtyping","volume":"9","author":"Palsberg J.","year":"1997","unstructured":"Palsberg , J. , Wand , M. , and O'Keefe , P. M. 1997 . Type inference with non-structural subtyping . Form. Asp. Comput. 9 , 49 -- 67 . Palsberg, J., Wand, M., and O'Keefe, P. M.1997. Type inference with non-structural subtyping. Form. Asp. Comput. 9, 49--67.","journal-title":"Form. Asp. Comput."},{"key":"e_1_2_1_25_1","first-page":"376","volume-title":"Annual Symposium on Logic in Computer Science (LICS'93)","author":"Pierce B.","unstructured":"Pierce , B. and Sangiorgi , D . 1993. Typing and subtyping for mobile processes . In Annual Symposium on Logic in Computer Science (LICS'93) , pp. 376 -- 385 . Pierce, B. and Sangiorgi, D.1993. Typing and subtyping for mobile processes. In Annual Symposium on Logic in Computer Science (LICS'93), pp. 376--385."},{"volume-title":"Types and Programming Languages","author":"Pierce B. C.","key":"e_1_2_1_26_1","unstructured":"Pierce , B. C. 2002. Types and Programming Languages . MIT Press , Cambridge, Mass . Pierce, B. C.2002. Types and Programming Languages. MIT Press, Cambridge, Mass."},{"key":"e_1_2_1_27_1","first-page":"122","volume-title":"Proceedings of ACM SIGPLAN International Conference on Functional Programming. ACM","author":"Pottier F.","unstructured":"Pottier , F. 1996. Simplifying subtyping constraints . In Proceedings of ACM SIGPLAN International Conference on Functional Programming. ACM , New York , pp. 122 -- 133 . 10.1145\/232627.232642 Pottier, F.1996. Simplifying subtyping constraints. In Proceedings of ACM SIGPLAN International Conference on Functional Programming. ACM, New York, pp. 122--133. 10.1145\/232627.232642"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the European Symposium on Programming (Mar.)","author":"R\u00e9my D.","unstructured":"R\u00e9my , D. 1998. From classes to objects via subtyping . In Proceedings of the European Symposium on Programming (Mar.) . Lecture Notes in Computer Science , vol. 1381 . Springer-Verlag , New York . R\u00e9my, D.1998. From classes to objects via subtyping. In Proceedings of the European Symposium on Programming (Mar.). Lecture Notes in Computer Science, vol. 1381. Springer-Verlag, New York."},{"key":"e_1_2_1_30_1","unstructured":"Tang F. and Hofmann M.2001. Type inference for objects with base types. Draft.  Tang F. and Hofmann M.2001. Type inference for objects with base types. Draft."},{"volume-title":"Proceedings of FOOL'02","author":"Tang F.","key":"e_1_2_1_31_1","unstructured":"Tang , F. and Hofmann , M . 2002. Generation of verification conditions for Abadi and Leino's logic of objects . In Proceedings of FOOL'02 , Ninth International Workshop on Foundations of Object-Oriented Languages (Portland, Ore., Jan.). Tang, F. and Hofmann, M.2002. Generation of verification conditions for Abadi and Leino's logic of objects. In Proceedings of FOOL'02, Ninth International Workshop on Foundations of Object-Oriented Languages (Portland, Ore., Jan.)."},{"key":"e_1_2_1_32_1","first-page":"308","volume-title":"Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS'92)","author":"Tiuryn J.","unstructured":"Tiuryn , J. 1992. Subtype inequalities . In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS'92) . IEEE Computer Society Press, Los Alamitos, Calif. , pp. 308 -- 315 . Tiuryn, J.1992. Subtype inequalities. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS'92). IEEE Computer Society Press, Los Alamitos, Calif., pp. 308--315."},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1017\/S0960129500000815","article-title":"Strong normalization with non-structural subtyping","volume":"5","author":"Wand M.","year":"1995","unstructured":"Wand , M. , O'Keefe , P. M. , and Palsberg , J. 1995 . Strong normalization with non-structural subtyping . Math. Struct. Comput. Sci. 5 , 3, 419 -- 430 . Wand, M., O'Keefe, P. M., and Palsberg, J.1995. Strong normalization with non-structural subtyping. Math. Struct. Comput. Sci. 5, 3, 419--430.","journal-title":"Math. Struct. Comput. Sci."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1053468.1053472","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1053468.1053472","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:07:53Z","timestamp":1750262873000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1053468.1053472"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["10.1145\/1053468.1053472"],"URL":"https:\/\/doi.org\/10.1145\/1053468.1053472","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2005,1]]},"assertion":[{"value":"2005-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}