{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:00:18Z","timestamp":1767927618588,"version":"3.49.0"},"reference-count":67,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2007,3,1]],"date-time":"2007-03-01T00:00:00Z","timestamp":1172707200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2007,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0956796806006216_inline1\"><jats:alt-text>${\\cal L}$<\/jats:alt-text><\/jats:inline-graphic>that is completely separate from run-time programs, leading to the DML(<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0956796806006216_inline1\"><jats:alt-text>${\\cal L}$<\/jats:alt-text><\/jats:inline-graphic>) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.<\/jats:p>","DOI":"10.1017\/s0956796806006216","type":"journal-article","created":{"date-parts":[[2006,12,11]],"date-time":"2006-12-11T12:37:18Z","timestamp":1165840638000},"page":"215-286","source":"Crossref","is-referenced-by-count":52,"title":["Dependent ML An approach to practical programming with dependent types"],"prefix":"10.1017","volume":"17","author":[{"given":"HONGWEI","family":"XI","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,3,1]]},"reference":[{"key":"S0956796806006216_N1087F","volume-title":"Pages 214\u2013227 of: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages","author":"Xi","year":"1999"},{"key":"S0956796806006216_N10861","doi-asserted-by":"crossref","unstructured":"Xi H. & Pfenning F. (1998) Eliminating array bound checking through dependent types. Pages 249\u2013257 of: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation.","DOI":"10.1145\/277650.277732"},{"key":"S0956796806006216_N1084A","unstructured":"Xi H. (2005) Applied Type System. Available at: http:\/\/www.cs.bu.edu\/hwxi\/ATS."},{"key":"S0956796806006216_N107C3","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"S0956796806006216_N10784","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"S0956796806006216_N10742","doi-asserted-by":"publisher","DOI":"10.1145\/322033.322034"},{"key":"S0956796806006216_N1072F","doi-asserted-by":"crossref","unstructured":"Sheard T. (2004) Languages of the future. Proceedings of the Onward! Track of Objected-oriented Programming Systems, Languages, Applications (OOPSLA). Vancouver, BC: ACM Press.","DOI":"10.1145\/1028664.1028711"},{"key":"S0956796806006216_N106F1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58601-6_109"},{"key":"S0956796806006216_N10696","doi-asserted-by":"crossref","unstructured":"Pierce B. & Turner D. (1998) Local type inference. Pages 252\u2013265 of: Proceedings of 25th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '98).","DOI":"10.1145\/268946.268967"},{"key":"S0956796806006216_N10678","doi-asserted-by":"crossref","unstructured":"Pfenning F. & Elliott C. (1988) Higher-order abstract syntax. Pages 199\u2013208 of: Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation.","DOI":"10.1145\/53990.54010"},{"key":"S0956796806006216_N1063A","doi-asserted-by":"crossref","unstructured":"Parent C. (1995) Synthesizing proofs from programs in the calculus of inductive constructions. Pages 351\u2013379 of: Proceedings of the International Conference on Mathematics for Programs Constructions. Springer-Verlag LNCS 947.","DOI":"10.1007\/3-540-60117-1_20"},{"key":"S0956796806006216_N105F0","volume-title":"Pages 411\u2013414 of","author":"Owre","year":"1996"},{"key":"S0956796806006216_N105DB","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"S0956796806006216_N10558","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0956796806006216_N1052B","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (revised)","author":"Milner","year":"1997"},{"key":"S0956796806006216_N10518","unstructured":"Michaylov S. (1992) Design and implementation of practical constraint logic programming systems. Ph.D. thesis, Carnegie Mellon University. Available as Technical Report CMU-CS-92-168."},{"key":"S0956796806006216_N104D9","unstructured":"McBride C. Epigram. Available at: http:\/\/www.dur.ac.uk\/CARG\/epigram."},{"key":"S0956796806006216_N104B9","volume-title":"Mathematical logic and programming languages","author":"Martin-L\u00f6f","year":"1985"},{"key":"S0956796806006216_N10443","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004026"},{"key":"S0956796806006216_N107FB","unstructured":"Xi H. (1999) Dependently Typed Data Structures. Pages 17\u201333 of: Proceedings of Workshop on Algorithmic Aspects of Advanced Programming Languages."},{"key":"S0956796806006216_N1041B","unstructured":"Jones S. P. , Vytiniotis D. , Weirich S. & Washburn G. (2005) Simple Unification-based Type Inference for GADTS."},{"key":"S0956796806006216_N10401","unstructured":"Jay C. B. & Sekanina M. (1996) Shape checking of array programs. Tech. rept. 96.09. University of Technology, Sydney, Australia."},{"key":"S0956796806006216_N103F5","unstructured":"INRIA. Objective Caml. http:\/\/caml.inria.fr."},{"key":"S0956796806006216_N103D4","doi-asserted-by":"crossref","unstructured":"Hughes J. , Pareto L. & Sabry A. (1996) Proving the Correctness of Reactive Systems Using Sized Types. Pages 410\u2013423 of: Proceeding of 23rd Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '96).","DOI":"10.1145\/237721.240882"},{"key":"S0956796806006216_N103B3","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680100404X"},{"key":"S0956796806006216_N10395","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"S0956796806006216_N1057F","volume-title":"Categories in Computer Science and Logic","author":"Mitchell","year":"1989"},{"key":"S0956796806006216_N1064D","unstructured":"Peyton Jones, S. . (1999) Haskell 98 \u2013 A non-strict, purely functional language. Available at http:\/\/www.haskell.org\/onlinereport\/."},{"key":"S0956796806006216_N10763","unstructured":"Sulzmann M. , Odersky M. & Wehr M. (1997) Type inference with constrained types. Proceedings of 4th International Workshop on Foundations of Object-oriented Languages."},{"key":"S0956796806006216_N108CA","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00062-5"},{"key":"S0956796806006216_N100B2","doi-asserted-by":"publisher","DOI":"10.2307\/2272981"},{"key":"S0956796806006216_N10666","volume-title":"Computation and Deduction","author":"Pfenning"},{"key":"S0956796806006216_N1035B","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"S0956796806006216_N104A1","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796806006216_N10710","volume-title":"Toward formal development of ML programs: Foundations and methodology","author":"Sannella","year":"1989"},{"key":"S0956796806006216_N10313","doi-asserted-by":"crossref","unstructured":"Freeman T. & Pfenning F. (1991) Refinement types for ML. Pages 268\u2013277 of: ACM SIGPLAN Conference on Programming Language Design and Implementation.","DOI":"10.1145\/113445.113468"},{"key":"S0956796806006216_N10186","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005617"},{"key":"S0956796806006216_N108E8","unstructured":"Zenger C. (1998) Indizierte typen. Ph.D. thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe."},{"key":"S0956796806006216_N10331","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionnelle et \u00c9limination des coupures dans l'arith-m\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Paris VII, Paris, France."},{"key":"S0956796806006216_N106D2","volume-title":"Pages 140\u2013151 of: ACM SIGPLAN '92 Conference on Programming Language Design and Implementation","author":"Pugh","year":"1992"},{"key":"S0956796806006216_N10344","doi-asserted-by":"crossref","unstructured":"Griffin T. (1990) A Formulae-as-Types Notion of Control. Pages 47\u201358 of: Conference Record of POPL '90: 17th ACM SIGPLAN Symposium on Principles of Programming Languages.","DOI":"10.1145\/96709.96714"},{"key":"S0956796806006216_N106B4","doi-asserted-by":"crossref","unstructured":"Pottier F. & R\u00e9gis-Gianas Y. (2006) Stratified type inference for generalized algebraic data types. Pages 232\u2013244 of: Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL'06).","DOI":"10.1145\/1111037.1111058"},{"key":"S0956796806006216_N1014A","doi-asserted-by":"crossref","unstructured":"Chen C. & Xi H. (2003) Implementing Typeful Program Transformations. Pages 20\u201328 of: Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics based Program Manipulation.","DOI":"10.1145\/777388.777392"},{"key":"S0956796806006216_N102B2","volume-title":"Combining two forms of type refinement","author":"Dunfield","year":"2002"},{"key":"S0956796806006216_N107E4","unstructured":"Xi H. (1998) Dependent types in practical programming. Ph.D. thesis, Carnegie Mellon University. pp. viii+189. Available at http:\/\/www.cs.cmu.edu\/hwxi\/DML\/thesis.ps."},{"key":"S0956796806006216_N10464","volume-title":"15th International Conference on Automated Deduction","author":"Kreitz","year":"1998"},{"key":"S0956796806006216_N107A2","doi-asserted-by":"crossref","unstructured":"Westbrook E. , Stump A. & Wehrman I. (2005) A Language-Based Approach to Functionally Correct Imperative Programming. Pages 268\u2013279 of: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming.","DOI":"10.1145\/1086365.1086400"},{"key":"S0956796806006216_N101AD","unstructured":"Chen C. , Shi R. & Xi H. (2005) Implementing Typeful Program Transformations. Fundamenta informaticae, 69(1\u20132), 103\u2013121."},{"key":"S0956796806006216_N10228","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"S0956796806006216_N100D0","volume-title":"An Introduction to Mathematical Logic: To Truth through Proof","author":"Andrews","year":"1986"},{"key":"S0956796806006216_N10812","first-page":"851","article-title":"Dependently Typed Pattern Matching","volume":"9","author":"Xi","year":"2003","journal-title":"Journal of Universal Computer Science"},{"key":"S0956796806006216_N100E8","doi-asserted-by":"crossref","unstructured":"Augustsson L. (1998) Cayenne \u2013 a language with dependent types. Pages 239\u2013250 of: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming.","DOI":"10.1145\/291251.289451"},{"key":"S0956796806006216_N100FA","volume-title":"The lambda calculus, its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0956796806006216_N10115","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"S0956796806006216_N10168","doi-asserted-by":"crossref","unstructured":"Chen C. & Xi H. (2005a) Combining Programming with Theorem Proving. Pages 66\u201377 of: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming.","DOI":"10.1145\/1086365.1086375"},{"key":"S0956796806006216_N104ED","volume-title":"Pages 219\u2013224 of:","author":"Meyer","year":"1985"},{"key":"S0956796806006216_N101D2","unstructured":"Cheney J. & Hinze R. (2003) Phantom Types. Technical Report CUCIS-TR2003-1901. Cornell University. Available at http:\/\/techreports.library.cornell.edu:8081\/Dienst\/UI\/1.0\/Display\/cul.cis\/TR2003-1901."},{"key":"S0956796806006216_N101F0","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796806006216_N1020E","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"Constable","year":"1986"},{"key":"S0956796806006216_N1024D","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003104"},{"key":"S0956796806006216_N10833","unstructured":"Xi H. (2004) Applied Type System (extended abstract). Pages 394\u2013408 of: Post-Workshop Proceedings of Types 2003. Springer-Verlag LNCS 3085."},{"key":"S0956796806006216_N1026E","unstructured":"Dowek G. , Felty A. , Herbelin H. , Huet G. , Murthy C. , Parent C. , Paulin-Mohring C. & Werner B. (1993) The Coq proof assistant user's guide. Rapport Technique 154. INRIA, Rocquencourt, France. Version 5.8."},{"key":"S0956796806006216_N105B5","volume-title":"Pages 41\u201353 of","author":"Odersky","year":"2001"},{"key":"S0956796806006216_N102CA","volume-title":"Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'03)","author":"Dunfield","year":"2003"},{"key":"S0956796806006216_N108A1","volume-title":"Pages 224\u2013235 of: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages","author":"Xi","year":"2003"},{"key":"S0956796806006216_N102F5","doi-asserted-by":"crossref","unstructured":"Dunfield J. & Pfenning F. (2004) Tridirectional typechecking. Pages 281\u2013292 of: Leroy, X. (ed), Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04). Venice, Italy: ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004.","DOI":"10.1145\/964001.964025"},{"key":"S0956796806006216_N10379","volume-title":"PX: A computational logic","author":"Hayashi","year":"1988"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796806006216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T21:04:17Z","timestamp":1555967057000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796806006216\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3]]},"references-count":67,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,3]]}},"alternative-id":["S0956796806006216"],"URL":"https:\/\/doi.org\/10.1017\/s0956796806006216","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,3]]}}}