{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:11:36Z","timestamp":1784200296025,"version":"3.55.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    We present the first sound and complete decision procedure capable of validating nominal object-oriented programs without type annotations in expressions even in the presence of generic interfaces with irregularlyrecursive signatures. Such interface signatures are exemplary of the challenges an algorithm must overcome in order to scale to the needs of modern major typed object-oriented languages. We do so by incorporating event-driven\n                    <jats:italic toggle=\"yes\">label-listeners<\/jats:italic>\n                    into our constraint system, enabling more complex aspects of program validation to be generated on demand while still ensuring termination. Furthermore, we define\n                    <jats:italic toggle=\"yes\">type-consistency<\/jats:italic>\n                    as a novel declarative notion of program validity that ensures safety without requiring a complex grammar of types to perform inference within. While type-inferability ensures type-consistency, the converse does not necessarily hold. Thus our algorithm decides program validity without inferring the types missing from the program, and so we instead call it a\n                    <jats:italic toggle=\"yes\">type-outference<\/jats:italic>\n                    algorithm. By bypassing type-inference, the proofs involving type-consistency more directly connect the design of and reasoning about constraints to the operational semantics of the language, simplifying much of the design and verification process. We mechanically formalize and verify these concepts and techniques\u2014type-consistency, type-outference, and label-listeners\u2014in Rocq to provide a solid foundation for scaling decidability beyond the limitations of structural types.\n                  <\/jats:p>","DOI":"10.1145\/3763797","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3784-3810","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7608-4605","authenticated-orcid":false,"given":"Ross","family":"Tate","sequence":"first","affiliation":[{"name":"Independent Researcher and Consultant, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165188"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546196.3550163"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951928"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632932"},{"key":"e_1_3_1_7_1","unstructured":"Stephen Dolan. 2017. Algebraic Subtyping. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/217838.217858"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80008-2"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19027-9_7"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_35"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90144-7"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594308"},{"key":"e_1_3_1_15_1","unstructured":"Trevor Jim and Jens Palsberg. 1999. Type inference in systems of recursive types with subtyping. (1999). https:\/\/web.cs.ucla.edu\/~palsberg\/draft\/jim-palsberg99.pdf"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141540"},{"key":"e_1_3_1_17_1","unstructured":"Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. (Jan. 2007). https:\/\/www.microsoft.com\/en-us\/research\/publication\/on-decidability-of-nominal-subtyping-with-variance\/"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen Jens Palsberg and Michael I. Schwartzbach. 1994. Efficient Inference of Partial Types. J. Comput. System Sci. 49 2 (1994) 306\u2013324. doi:10.1016\/S0022-0000(05)80051-0","DOI":"10.1016\/S0022-0000(05)80051-0"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199533"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90196-3"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Jens Palsberg and Michael I. Schwartzbach. 1995. Safety Analysis versus Type Inference. Information and Computation 118 1 (1995) 128\u2013141. doi:10.1006\/inco.1995.1058","DOI":"10.1006\/inco.1995.1058"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212524"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_1_26_1","unstructured":"Pierre-Marie P\u00e9drot. 2015. Issue coq\/coq#4261: Nested coinductive types are useless. (June 2015). https:\/\/github.com\/coq\/coq\/issues\/4261"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143228"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289448"},{"key":"e_1_3_1_29_1","unstructured":"Fran\u00e7ois Pottier. 1998b. Type Inference in the Presence of Subtyping: From Theory to Practice. Ph. D. Dissertation. Institut National de Recherche en Informatique et en Automatique. https:\/\/inria.hal.science\/inria-00073205"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_120"},{"key":"e_1_3_1_31_1","unstructured":"Geoffrey Seward Smith. 1991. Polymorphic Type Inference for Languages with Overloading and Subtyping. Ph. D. Dissertation. Cornell University. https:\/\/hdl.handle.net\/1813\/7070"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73568"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Ross Tate. 2025. Rocq Formalization and Verification for the OOPSLA 2025 Article \u2018Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics\u2019. doi:10.1145\/3747411","DOI":"10.1145\/3747411"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_98"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_52"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:15:34Z","timestamp":1784196934000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":34,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763797"],"URL":"https:\/\/doi.org\/10.1145\/3763797","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}