{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:38:06Z","timestamp":1770273486965,"version":"3.49.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319309354","type":"print"},{"value":"9783319309361","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30936-1_14","type":"book-chapter","created":{"date-parts":[[2016,3,29]],"date-time":"2016-03-29T16:27:44Z","timestamp":1459268864000},"page":"249-272","source":"Crossref","is-referenced-by-count":44,"title":["The Essence of Dependent Object Types"],"prefix":"10.1007","author":[{"given":"Nada","family":"Amin","sequence":"first","affiliation":[]},{"given":"Samuel","family":"Gr\u00fctter","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Odersky","sequence":"additional","affiliation":[]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[]},{"given":"Sandro","family":"Stucki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,25]]},"reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"RM Amadio","year":"1993","unstructured":"Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575\u2013631 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR2","unstructured":"Amin, N., Moors, A., Odersky, M.: Dependent object types. In: FOOL (2012)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: OOPSLA (2014)","DOI":"10.1145\/2660193.2660216"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995)","DOI":"10.1145\/199448.199507"},{"issue":"1\/2","key":"14_CR5","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1006\/inco.1994.1013","volume":"109","author":"L Cardelli","year":"1994","unstructured":"Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. Inf. Comput. 109(1\/2), 4\u201356 (1994)","journal-title":"Inf. Comput."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Tribe: a simple virtual class calculus. In: AOSD (2007)","DOI":"10.1145\/1218563.1218578"},{"key":"14_CR7","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-09510-1_11","volume-title":"Automata, Languages and Programming","author":"M. Coppo","year":"1979","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Sall\u00e9, P.: Functional characterization of some semantic equalities inside lambda-calculus. In: Automata, Languages and Programming, 6th Colloquium (1979)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11821069_1","volume-title":"Mathematical Foundations of Computer Science 2006","author":"V Cremet","year":"2006","unstructured":"Cremet, V., Garillot, F., Lenglet, S., Odersky, M.: A core calculus for scala type checking. In: Kr\u00e1lovi\u010d, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 1\u201323. Springer, Heidelberg (2006)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Cretin, J., R\u00e9my, D.: System F with coercion constraints. In: CSL-LICS (2014)","DOI":"10.1145\/2603088.2603128"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Rossberg, A.: Mixin\u2019 up the ML module system. In: ICFP (2008)","DOI":"10.1145\/1411204.1411248"},{"key":"14_CR11","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 - Object-Oriented Programming","author":"E Ernst","year":"2001","unstructured":"Ernst, E.: Family polymorphism. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 303. Springer, Heidelberg (2001)"},{"key":"14_CR12","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-540-45070-2_14","volume-title":"ECOOP 2003 \u2013 Object-Oriented Programming","author":"Erik Ernst","year":"2003","unstructured":"Ernst, E.: Higher-order hierarchies. In: ECOOP (2003)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: POPL (2006)","DOI":"10.1145\/1111037.1111062"},{"issue":"1","key":"14_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL (1994)","DOI":"10.1145\/174675.176927"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-47993-7_19","volume-title":"ECOOP 2002 - Object-Oriented Programming","author":"B Adsul","year":"2002","unstructured":"Adsul, B., Viroli, M.: On variance-based subtyping for parametric types. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, p. 441. Springer, Heidelberg (2002)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Manifest types, modules and separate compilation. In: POPL (1994)","DOI":"10.1145\/174675.176926"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Macqueen, D.: Using dependent types to express modular structure. In: POPL (1986)","DOI":"10.1145\/512644.512670"},{"issue":"1","key":"14_CR19","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1145\/1594834.1480926","volume":"44","author":"Beno\u00eet Montagu","year":"2009","unstructured":"Montagu, B., R\u00e9my, D.: Modeling abstract types in modules with open existential types. In: POPL (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR20","unstructured":"Moors, A., Piessens, F., Odersky, M.: Safe type-level abstraction in scala. In: FOOL (2008)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Odersky, M., Cremet, V., R\u00f6ckl, C., Zenger, M.: A nominal theory of objects with dependent types. In: ECOOP (2003)","DOI":"10.1007\/978-3-540-45070-2_10"},{"key":"14_CR22","unstructured":"Odersky, M., Petrashko, D., Martres, G., others.: The dotty project (2013). \n                    https:\/\/github.com\/lampepfl\/dotty"},{"key":"14_CR23","unstructured":"van der Ploeg, A.: The HMap package (2013). \n                    https:\/\/hackage.haskell.org\/package\/HMap"},{"key":"14_CR24","unstructured":"Pretty, J.: Minimizing the slippery surface of failure. Talk at Scala World (2015). \n                    https:\/\/www.youtube.com\/watch?v=26UHdZUsKkE"},{"key":"14_CR25","unstructured":"Rompf, T., Amin, N.: From F to DOT: Type soundness proofs with definitional interpreters. Purdue University, Technical report (2015). \n                    http:\/\/arxiv.org\/abs\/1510.05216"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Rossberg, A.: 1ML - core and modules united (f-ing first-class modules). In: ICFP (2015)","DOI":"10.1145\/2784731.2784738"},{"issue":"5","key":"14_CR27","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1017\/S0956796814000264","volume":"24","author":"A Rossberg","year":"2014","unstructured":"Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. J. Funct. Program. 24(5), 529\u2013607 (2014)","journal-title":"J. Funct. Program."},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1007\/978-3-662-46669-8_28","volume-title":"Programming Languages and Systems","author":"G Scherer","year":"2015","unstructured":"Scherer, G., R\u00e9my, D.: Full reduction in the face of absurdity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 685\u2013709. Springer, Heidelberg (2015)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Tate, R., Leung, A., Lerner, S.: Taming wildcards in java\u2019s type system. In: PLDI (2011)","DOI":"10.1145\/1993498.1993570"},{"key":"14_CR30","unstructured":"Torgersen, M., Ernst, E., Hansen, C.P.: WildFJ. In: FOOL (2004)"}],"container-title":["Lecture Notes in Computer Science","A List of Successes That Can Change the World"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30936-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T18:36:13Z","timestamp":1559414173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30936-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319309354","9783319309361"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30936-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}