{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:10Z","timestamp":1751662870063,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Oracle Labs Australia","award":["1630"],"award-info":[{"award-number":["1630"]}]},{"DOI":"10.13039\/100000005","name":"US Department of Defense","doi-asserted-by":"crossref","award":["H98230-14-C-0140"],"award-info":[{"award-number":["H98230-14-C-0140"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Path dependent types have long served as an expressive component of the Scala programming language. They allow for the modelling of both bounded polymorphism and a degree of nominal subtyping. Nominality in turn provides the ability to capture first class modules. Thus a single language feature gives rise to a rich array of expressiveness. Recent work has proven path dependent types sound in the presence of both intersection and recursive types, but unfortunately typing remains undecidable, posing problems for programmers who rely on the results of type checkers. The Wyvern programming language is an object oriented language with path dependent types, recursive types and first class modules. In this paper we define two variants of Wyvern that feature decidable typing, along with machine checked proofs of decidability. Despite the restrictions, our approaches retain the ability to encode the parameteric polymorphism of Java generics along with many idioms of the Scala module system.<\/jats:p>","DOI":"10.1145\/3371134","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Decidable subtyping for path dependent types"],"prefix":"10.1145","volume":"4","author":[{"given":"Julian","family":"Mackay","sequence":"first","affiliation":[{"name":"Victoria University of Wellington, New Zealand"}]},{"given":"Alex","family":"Potanin","sequence":"additional","affiliation":[{"name":"Victoria University of Wellington, New Zealand"}]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[{"name":"Victoria University of Wellington, New Zealand"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_2_1","volume-title":"Martin Odersky, Tiark Rompf, and Sandro Stucki.","author":"Amin Nada","year":"2016","unstructured":"Nada Amin , Karl Samuel Gr\u00fctter , Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016 . The Essence of Dependent Object Types. A List of Successes That Can Change the World : Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday ( 2016), 249\u2013272. Nada Amin, Karl Samuel Gr\u00fctter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (2016), 249\u2013272."},{"key":"e_1_2_2_3_1","volume-title":"19th International Workshop on Foundations of Object-Oriented Languages.","author":"Amin Nada","year":"2012","unstructured":"Nada Amin , Adriaan Moors , and Martin Odersky . 2012 . Dependent object types . In 19th International Workshop on Foundations of Object-Oriented Languages. Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent object types. In 19th International Workshop on Foundations of Object-Oriented Languages."},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Nada Amin Tiark Rompf and Martin Odersky. 2014. Foundations of Path-dependent Types. In OOPSLA \u201914.  Nada Amin Tiark Rompf and Martin Odersky. 2014. Foundations of Path-dependent Types. In OOPSLA \u201914.","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_2_5_1","volume-title":"A Network Protocol Stack in Standard ML. Higher-Order and Symbolic Computation","author":"Biagioni Edoardo","year":"2001","unstructured":"Edoardo Biagioni , Robert Harper , and Peter Lee . 2001. A Network Protocol Stack in Standard ML. Higher-Order and Symbolic Computation ( 2001 ). Edoardo Biagioni, Robert Harper, and Peter Lee. 2001. A Network Protocol Stack in Standard ML. Higher-Order and Symbolic Computation (2001)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_2_7_1","volume-title":"Pierce","author":"Castagna Giuseppe","year":"1994","unstructured":"Giuseppe Castagna and Benjamin C . Pierce . 1994 . Decidable Bounded Quantification. In POPL \u201994. Giuseppe Castagna and Benjamin C. Pierce. 1994. Decidable Bounded Quantification. In POPL \u201994."},{"key":"e_1_2_2_8_1","unstructured":"William R. Cook. 2009. On Understanding Data Abstraction Revisited. In OOPSLA \u201909.  William R. Cook. 2009. On Understanding Data Abstraction Revisited. In OOPSLA \u201909."},{"key":"e_1_2_2_9_1","volume-title":"Family Polymorphism. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP \u201901)","author":"Ernst Erik","year":"2001","unstructured":"Erik Ernst . 2001 . Family Polymorphism. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP \u201901) . Erik Ernst. 2001. Family Polymorphism. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP \u201901)."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594308"},{"key":"e_1_2_2_11_1","volume-title":"Java Generics Are Turing Complete. In POPL","author":"Grigore Radu","year":"2017","unstructured":"Radu Grigore . 2017 . Java Generics Are Turing Complete. In POPL 2017. Radu Grigore. 2017. Java Generics Are Turing Complete. In POPL 2017."},{"volume-title":"Practical Foundations for Programming Languages","author":"Harper Robert","key":"e_1_2_2_12_1","unstructured":"Robert Harper . 2012. Practical Foundations for Programming Languages . Cambridge University Press , New York, NY, USA . Robert Harper. 2012. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_2_13_1","volume-title":"Undecidability of D &lt","author":"Hu Jason","year":"2020","unstructured":"Jason Hu and Ond\u0159ej Lhot\u00e1k . 2020. Undecidability of D &lt ; : and its Decidable Fragments. In POPL 2020 . Jason Hu and Ond\u0159ej Lhot\u00e1k. 2020. Undecidability of D &lt; : and its Decidable Fragments. In POPL 2020."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2942"},{"key":"e_1_2_2_15_1","volume-title":"The BETA Programming Language. DAIMI Report Series 16, 229","author":"Kristensen Bent","year":"1987","unstructured":"Bent Kristensen , Ole Madsen , Birger M\u00f8ller-Pedersen , and Kristen Nygaard . 1987. The BETA Programming Language. DAIMI Report Series 16, 229 ( 1987 ). Bent Kristensen, Ole Madsen, Birger M\u00f8ller-Pedersen, and Kristen Nygaard. 1987. The BETA Programming Language. DAIMI Report Series 16, 229 (1987)."},{"key":"e_1_2_2_16_1","volume-title":"Virtual Classes: A Powerful Mechanism in Object-oriented Programming. In OOPSLA \u201989.","author":"Madsen O. L.","year":"1989","unstructured":"O. L. Madsen and B. Moller-Pedersen . 1989 . Virtual Classes: A Powerful Mechanism in Object-oriented Programming. In OOPSLA \u201989. O. L. Madsen and B. Moller-Pedersen. 1989. Virtual Classes: A Powerful Mechanism in Object-oriented Programming. In OOPSLA \u201989."},{"key":"e_1_2_2_17_1","volume-title":"31st European Conference on Object-Oriented Programming (ECOOP","author":"Melicher Darya","year":"2017","unstructured":"Darya Melicher , Yangqingwei Shi , Alex Potanin , and Jonathan Aldrich . 2017 . A Capability-Based Module System for Authority Control . In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A Capability-Based Module System for Authority Control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017)."},{"volume-title":"Revised Edition","author":"Milner Robin","key":"e_1_2_2_18_1","unstructured":"Robin Milner , Robert Harper , David MacQueen , and Mads Tofte . 1997. The Definition of Standard ML , Revised Edition . MIT Press . Robin Milner, Robert Harper, David MacQueen, and Mads Tofte. 1997. The Definition of Standard ML, Revised Edition. MIT Press."},{"key":"e_1_2_2_19_1","volume-title":"Empowering Union and Intersection Types with Integrated Subtyping. In OOPSLA","author":"Muehlboeck Fabian","year":"2018","unstructured":"Fabian Muehlboeck and Ross Tate . 2018 . Empowering Union and Intersection Types with Integrated Subtyping. In OOPSLA 2018. Fabian Muehlboeck and Ross Tate. 2018. Empowering Union and Intersection Types with Integrated Subtyping. In OOPSLA 2018."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136003"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489828.2489830"},{"key":"e_1_2_2_22_1","unstructured":"Martin Odersky Philippe Altherr Vincent Cremet Burak Emir Stphane Micheloud Nikolay Mihaylov Michel Schinz Erik Stenman and Matthias Zenger. 2004. The Scala language specification.  Martin Odersky Philippe Altherr Vincent Cremet Burak Emir Stphane Micheloud Nikolay Mihaylov Michel Schinz Erik Stenman and Matthias Zenger. 2004. The Scala language specification."},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Martin Odersky and Matthias Zenger. 2005. Scalable Component Abstractions. In OOPSLA \u201905.  Martin Odersky and Matthias Zenger. 2005. Scalable Component Abstractions. In OOPSLA \u201905.","DOI":"10.1145\/1094811.1094815"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Cyrus Omar Darya Kurilova Ligia Nistor Benjamin Chung Alex Potanin and Jonathan Aldrich. 2014. Safely Composable Type-Specific Languages. In ECOOP \u201914.  Cyrus Omar Darya Kurilova Ligia Nistor Benjamin Chung Alex Potanin and Jonathan Aldrich. 2014. Safely Composable Type-Specific Languages. In ECOOP \u201914.","DOI":"10.1007\/978-3-662-44202-9_5"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In POPL \u201992.  Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In POPL \u201992.","DOI":"10.1145\/143165.143228"},{"key":"e_1_2_2_26_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages ( 1 st ed.). The MIT Press . Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.","edition":"1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133870"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"volume-title":"ECOOP\u201997 \u2014 Object-Oriented Programming, Mehmet Ak\u015fit and Satoshi Matsuoka (Eds.)","author":"Thorup Kresten Krab","key":"e_1_2_2_30_1","unstructured":"Kresten Krab Thorup . 1997. Genericity in java with virtual types . In ECOOP\u201997 \u2014 Object-Oriented Programming, Mehmet Ak\u015fit and Satoshi Matsuoka (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 444\u2013471. Kresten Krab Thorup. 1997. Genericity in java with virtual types. In ECOOP\u201997 \u2014 Object-Oriented Programming, Mehmet Ak\u015fit and Satoshi Matsuoka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 444\u2013471."},{"key":"e_1_2_2_31_1","volume-title":"5th Workshop on Foundations of Object-Oriented Languages","volume":"544","author":"Torgersen Mads","year":"1998","unstructured":"Mads Torgersen . 1998 . Virtual types are statically safe . In 5th Workshop on Foundations of Object-Oriented Languages , Vol. 544 . Citeseer, 1\u20139. Mads Torgersen. 1998. Virtual types are statically safe. In 5th Workshop on Foundations of Object-Oriented Languages, Vol. 544. Citeseer, 1\u20139."},{"key":"e_1_2_2_32_1","volume-title":"Nominal Wyvern: Employing Semantic Separation for Usability. Master\u2019s thesis","author":"Zhu Yu Xiang","year":"2019","unstructured":"Yu Xiang Zhu . 2019 . Nominal Wyvern: Employing Semantic Separation for Usability. Master\u2019s thesis . Carnegie Mellon University . Yu Xiang Zhu. 2019. Nominal Wyvern: Employing Semantic Separation for Usability. Master\u2019s thesis. Carnegie Mellon University."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371134","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371134","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371134"],"URL":"https:\/\/doi.org\/10.1145\/3371134","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}