{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:54:20Z","timestamp":1770281660834,"version":"3.49.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031210365","type":"print"},{"value":"9783031210372","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-21037-2_9","type":"book-chapter","created":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T00:05:14Z","timestamp":1669334714000},"page":"175-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Calculus with\u00a0Recursive Types, Record Concatenation and\u00a0Subtyping"],"prefix":"10.1007","author":[{"given":"Yaoda","family":"Zhou","sequence":"first","affiliation":[]},{"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[]},{"given":"Andong","family":"Fan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,11,25]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4419-8598-9"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-54434-1_1","volume-title":"Programming Languages and Systems","author":"J Alpuim","year":"2017","unstructured":"Alpuim, J., Oliveira, B.C.S., Shi, Z.: Disjoint polymorphism. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 1\u201328. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_1"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. OOPSLA 2014. Association for Computing Machinery (2014)","DOI":"10.1145\/2660193.2660216"},{"issue":"4","key":"9_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Logic 48(4), 931\u2013940 (1983)","journal-title":"J. Symb. Logic"},{"key":"9_CR5","unstructured":"Bi, X., Oliveira, B.C.d.S.: Typed first-class traits. In: 32nd European Conference on Object-Oriented Programming (ECOOP 2018) (2018)"},{"key":"9_CR6","unstructured":"Bi, X., Oliveira, B.C.d.S., Schrijvers, T.: The essence of nested composition. In: 32nd European Conference on Object-Oriented Programming (ECOOP 2018) (2018)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-030-17184-1_14","volume-title":"Programming Languages and Systems","author":"X Bi","year":"2019","unstructured":"Bi, X., Xie, N., Oliveira, B.C.S., Schrijvers, T.: Distributive disjoint polymorphism for compositional programming. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 381\u2013409. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_14"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-662-44202-9_11","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"G Bierman","year":"2014","unstructured":"Bierman, G., Abadi, M., Torgersen, M.: Understanding typescript. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 257\u2013281. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_11"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bruce, K., Cardeli, L., Castagna, G., Group, T.H.O., Leavens, G.T., Pierce, B.: On binary methods. Theory Pract. Object Syst. 1(3) (1996)","DOI":"10.1002\/j.1096-9942.1995.tb00019.x"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings 155(1\/2), 108\u2013133 (1999). http:\/\/www.cis.upenn.edu\/bcpierce\/papers\/compobj.ps","DOI":"10.1006\/inco.1999.2829"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: A semantics of multiple inheritance. In: Semantics of Data Types (1984)","DOI":"10.1007\/3-540-13346-1_2"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-17184-3_38","volume-title":"Combinators and Functional Programming Languages","author":"L Cardelli","year":"1986","unstructured":"Cardelli, L.: Amber. In: Cousineau, G., Curien, P.-L., Robinet, B. (eds.) LITP 1985. LNCS, vol. 242, pp. 21\u201347. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-17184-3_38"},{"key":"9_CR13","unstructured":"Cardelli, L.: Extensible Records in a Pure Calculus of Subtyping. Digital, Systems Research Center (1992)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: A language with distributed scope. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1995, pp. 286\u2013297 (1995)","DOI":"10.1145\/199448.199516"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0960129500000049","volume":"1","author":"L Cardelli","year":"1991","unstructured":"Cardelli, L., Mitchell, J.C.: Operations on records. Math. Struct. Comput. Sci. 1(1), 3\u201348 (1991)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Castagna, G., Frisch, A.: A gentle introduction to semantic subtyping. In: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 198\u2013199 (2005)","DOI":"10.1145\/1069774.1069793"},{"issue":"5","key":"9_CR17","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1017\/S0960129500070043","volume":"6","author":"AB Compagnoni","year":"1996","unstructured":"Compagnoni, A.B., Pierce, B.C.: Higher-order intersection types and multiple inheritance. Math. Struct. Comput. Sci. (MSCS) 6(5), 469\u2013501 (1996)","journal-title":"Math. Struct. Comput. Sci. (MSCS)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Cook, W.R., Hill, W., Canning, P.S.: Inheritance is not subtyping. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1990, pp. 125\u2013135 (1989)","DOI":"10.1145\/96709.96721"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Cook, W.R., Palsberg, J.: A denotational semantics of inheritance and its correctness. In: Object-Oriented Programming: Systems, Languages and Applications (OOPSLA) (1989)","DOI":"10.1145\/74877.74922"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/3-540-57887-0_121","volume-title":"Theoretical Aspects of Computer Software","author":"FM Damm","year":"1994","unstructured":"Damm, F.M.: Subtyping with union types, intersection types and recursive types. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 687\u2013706. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_121"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: International Conference on Functional Programming (ICFP) (2000)","DOI":"10.1145\/351240.351259"},{"issue":"2\u20133","key":"9_CR22","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1017\/S0956796813000270","volume":"24","author":"J Dunfield","year":"2014","unstructured":"Dunfield, J.: Elaborating intersection and union types. J. Funct. Program. 24(2\u20133), 133\u2013165 (2014)","journal-title":"J. Funct. Program."},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/3-540-45337-7_17","volume-title":"ECOOP 2001\u2014Object-Oriented Programming","author":"E Ernst","year":"2001","unstructured":"Ernst, E.: Family polymorphism. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 303\u2013326. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45337-7_17"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 137\u2013146. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029823"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Giarrusso, P.G., Stefanesco, L., Timany, A., Birkedal, L., Krebbers, R.: Scala step-by-step: soundness for dot with step-indexed logical relations in iris. Proc. ACM Program. Lang. 4(ICFP) (2020)","DOI":"10.1145\/zenodo.3926703"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Glew, N.: An efficient class and object encoding. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2000, pp. 311\u2013324. Association for Computing Machinery (2000)","DOI":"10.1145\/354222.353192"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Hu, J.Z., Lhot\u00e1k, O.: Undecidability of DSUB and its decidable fragments. Proc. ACM Program. Lang. 4(POPL), 1\u201330 (2019)","DOI":"10.1145\/3371077"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Huang, X., Oliveira, B.C.d.S.: A type-directed operational semantics for a calculus with a merge operator. In: 34th European Conference on Object-Oriented Programming (ECOOP 2020), vol. 166 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.26","DOI":"10.4230\/LIPIcs.ECOOP.2020.26"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Huang, X., Zhao, J., Oliveira, B.C.d.S.: Taming the merge operator: a type-directed operational semantics approach. J. Funct. Program. (2021)","DOI":"10.1017\/S0956796821000186"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Jones, T., Pearce, D.J.: A mechanical soundness proof for subtyping over recursive types. In: Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, pp. 1\u20136 (2016)","DOI":"10.1145\/2955811.2955812"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Mackay, J., Potanin, A., Aldrich, J., Groves, L.: Decidable subtyping for path dependent types. Proc. ACM Program. Lang. 4(POPL), 1\u201327 (2019)","DOI":"10.1145\/3371134"},{"key":"9_CR32","unstructured":"Microsoft: Typescript (2021). https:\/\/www.typescriptlang.org\/"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp. 364\u2013377 (2016)","DOI":"10.1145\/2951913.2951945"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Palsberg, J., Zhao, T.: Type inference for record concatenation and subtyping. Inf. Comput. 189(1) (2004)","DOI":"10.1016\/j.ic.2003.10.001"},{"issue":"12","key":"9_CR35","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/3170492.3136042","volume":"52","author":"DJ Pearce","year":"2017","unstructured":"Pearce, D.J.: Rewriting for sound and complete union, intersection and negation types. ACM SIGPLAN Not. 52(12), 117\u2013130 (2017)","journal-title":"ACM SIGPLAN Not."},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-02654-1_13","volume-title":"Software Language Engineering","author":"DJ Pearce","year":"2013","unstructured":"Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238\u2013248. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_13"},{"issue":"1","key":"9_CR37","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1994.1055","volume":"112","author":"BC Pierce","year":"1994","unstructured":"Pierce, B.C.: Bounded quantification is undecidable. Inf. Comput. 112(1), 131\u2013165 (1994)","journal-title":"Inf. Comput."},{"key":"9_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-46425-5_21","volume-title":"Programming Languages and Systems","author":"F Pottier","year":"2000","unstructured":"Pottier, F.: A 3-part type inference engine. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 320\u2013335. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_21"},{"key":"9_CR39","unstructured":"R\u00e9my, D.: A case study of typechecking with constrained types: typing record concatenation (1995). Presented at the Workshop on Advances in Types for Computer Science at the Newton Institute, Cambridge, UK"},{"key":"9_CR40","unstructured":"Reynolds, J.C.: Preliminary design of the programming language Forsythe (1988)"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Rompf, T., Amin, N.: Type soundness for dependent object types (DOT). In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 624\u2013641 (2016)","DOI":"10.1145\/2983990.2984008"},{"key":"9_CR42","unstructured":"The CoQ Development Team: CoQ (2019). https:\/\/coq.inria.fr"},{"key":"9_CR43","unstructured":"Wadler, P.: The expression problem (1998). Discussion on the Java Genericity mailing list"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Wang, F., Rompf, T.: Towards strong normalization for dependent object types (DOT). In: 31st European Conference on Object-Oriented Programming (ECOOP 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)","DOI":"10.1145\/2983990.2984008"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Zhang, W., Sun, Y., Oliveira, B.C.d.S.: Compositional programming. ACM Trans. Program. Lang. Syst. (TOPLAS), 1\u201360 (2021)","DOI":"10.1145\/3460228"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"Zhou, Y., Oliveira, B.C.d.S., Fan, A.: A calculus with recursive types, record concatenation and subtyping (artifact) (2022). https:\/\/doi.org\/10.5281\/zenodo.7003284","DOI":"10.5281\/zenodo.7003284"},{"key":"9_CR47","doi-asserted-by":"publisher","unstructured":"Zhou, Y., Zhao, J., Oliveira, B.C.d.S.: Revisiting ISO-recursive subtyping. ACM Trans. Program. Lang. Syst. (TOPLAS) (2022). https:\/\/doi.org\/10.1145\/3549537","DOI":"10.1145\/3549537"}],"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-031-21037-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T14:31:42Z","timestamp":1728484302000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21037-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031210365","9783031210372"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21037-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"25 November 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Auckland","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","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":"10","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":"45% - 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":"4","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":"4","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)"}}]}}