{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:57:59Z","timestamp":1770296279775,"version":"3.49.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1023\/a:1019916231463","type":"journal-article","created":{"date-parts":[[2003,3,15]],"date-time":"2003-03-15T13:06:10Z","timestamp":1047733570000},"page":"91-131","source":"Crossref","is-referenced-by-count":43,"title":["Dependent Types for Program Termination Verification"],"prefix":"10.1007","volume":"15","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5093031_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A. and Altenkirch, T. A predicative strong normalisation proof for a \u03bb-calculus with interleaving inductive types. In Proceedings of International Workshop on Types for Proof and Programs (TYPES '99), T. Coquand, P. Dybjer, B. Nordstr\u00f6m, and J. Smith (Eds.). LNCS,Vol. 1956, Springer-Verlag, 2000, pp. 21\u201340.","DOI":"10.1007\/3-540-44557-9_2"},{"issue":"2","key":"5093031_CR2","first-page":"137","volume":"9","author":"A. BenCherifa","year":"1987","unstructured":"BenCherifa, A. and Lescanne, P. Termination of rewriting systems by polynomial interpretations and its implementation. SCP, 9(2) (1987) 137\u2013160.","journal-title":"SCP"},{"key":"5093031_CR3","series-title":"Studies in Logic and Mathematical Foundations","volume-title":"Model Theory","author":"C.C. Chang","year":"1977","unstructured":"Chang, C.C. and Keisler, H.J. Model Theory, Studies in Logic and Mathematical Foundations, Vol. 73. North-Holland, Amsterdam, The Netherlands, 1977."},{"key":"5093031_CR4","unstructured":"Chin, W.-N. and Khoo, S.-C. Calculating sized types. Higher-Order and Symbolic Computation, 14(2\/3), to appear."},{"key":"5093031_CR5","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L. et al. Implementing Mathematics with the NuPrl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"5093031_CR6","doi-asserted-by":"crossref","unstructured":"Crary, K. and Weirich, S. Resource bound certification. In Proceedings of 27th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2000), Boston, 2000, pp. 184\u2013198.","DOI":"10.1145\/325694.325716"},{"issue":"3","key":"5093031_CR7","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N. Orderings for term rewriting systems. Theoretical Computer Science, 17(3) (1982) 279\u2013301.","journal-title":"Theoretical Computer Science"},{"key":"5093031_CR8","series-title":"Rapport Technique 154","volume-title":"The Coq proof assistant user's guide","author":"G. Dowek","year":"1993","unstructured":"Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., and Werner, B. The Coq proof assistant user's guide. Rapport Technique 154, INRIA, Rocquencourt, France. Version 5.8. 1993."},{"key":"5093031_CR9","volume-title":"Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures dans l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur","author":"J.-Y. Girard","year":"1972","unstructured":"Girard, J.-Y. Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures dans l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Paris VII, Paris, France, 1972."},{"key":"5093031_CR10","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., and Taylor, P. Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Vol. 7, Cambridge University Press, Cambridge, England, 1989."},{"key":"5093031_CR11","doi-asserted-by":"crossref","unstructured":"Grobauer, B. Cost recurrences for DML programs. In Proceedings of Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01), Florence, Italy, 2001, pp. 253\u2013264.","DOI":"10.1145\/507635.507666"},{"issue":"4","key":"5093031_CR12","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1017\/S0956796899003378","volume":"9","author":"R. Harper","year":"1999","unstructured":"Harper, R. Proof-directed debugging. Journal of Functional Programming, 9(4) (1999) 471\u2013477.","journal-title":"Journal of Functional Programming"},{"key":"5093031_CR13","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., and Sabry, A. Proving the correctness of reactive systems using sized types. In Conference Record of 23rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '96), 1996, pp. 410\u2013423.","DOI":"10.1145\/237721.240882"},{"key":"5093031_CR14","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P. and Rubio, A. The higher-order recursive path ordering. In Proceedings of 14th IEEE Symposium on Logic in Computer Science (LICS '99), Trento, Italy, 1999, pp. 402\u2013411.","DOI":"10.1109\/LICS.1999.782635"},{"key":"5093031_CR15","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., and Ben-Amram, A.M. The size-change principle for program termination. In Proceeding of the 28th ACM Symposium on Principles of Programming Languages (POPL '01), London, UK, 2001, pp. 81\u201392.","DOI":"10.1145\/360204.360210"},{"key":"5093031_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R.W., and MacQueen, D. The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts, 1997."},{"key":"5093031_CR17","first-page":"106","volume-title":"Conference Record of 24th Annual ACM Symposium on Principles of Programming Languages","author":"G. Necula","year":"1997","unstructured":"Necula, G. Proof-carrying code. In Conference Record of 24th Annual ACM Symposium on Principles of Programming Languages, ACM Press, Paris, France, 1997, pp. 106\u2013119."},{"key":"5093031_CR18","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Proceedings of the 8th International Conference on Computer-Aided Verification (CAV '96)","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. PVS: Combining specification, proof checking, and model checking. In Proceedings of the 8th International Conference on Computer-Aided Verification (CAV '96), R. Alur and T.A. Henzinger (Eds.). New Brunswick, NJ, LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 411\u2013414."},{"key":"5093031_CR19","doi-asserted-by":"crossref","unstructured":"Paulson, L. Isabelle: A Generic Theorem Prover. LNCS, Vol. 828, Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"5093031_CR20","doi-asserted-by":"crossref","unstructured":"Pientka, B. and Pfenning, F. Termination and reduction checking in the logical framework. In Proceedings of Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, PA, 2000.","DOI":"10.1007\/3-540-45744-5_32"},{"key":"5093031_CR21","first-page":"157","volume-title":"Proceedings of the 4th Static Analysis Symposium (SAS '97)","author":"C. Speirs","year":"1997","unstructured":"Speirs, C., Somogyi, Z., and S\u00f8ndergaard, H. Termination Analysis for Mercury. In Proceedings of the 4th Static Analysis Symposium (SAS '97), P.V. Hentenryck (Ed.). Paris, France, LNCS,Vol. 1302, Springer-Verlag, 1997, pp. 157\u2013171."},{"issue":"2","key":"5093031_CR22","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2) (1967) 198\u2013212.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"5093031_CR23","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1145\/42282.42285","volume":"35","author":"J.D. Ullman","year":"1988","unstructured":"Ullman, J.D. and Van Gelder, A. Efficient tests for top-down termination of logic rules. Journal of the ACM, 35(2) (1988) 345\u2013373.","journal-title":"Journal of the ACM"},{"key":"5093031_CR24","unstructured":"Xi, H. Dependent types in practical programming. Ph.D. Thesis, Carnegie Mellon University, 1998, pp. viii+189. Available as http:\/\/www.cs.cmu.edu\/~hwxi\/DML\/thesis.ps."},{"key":"5093031_CR25","unstructured":"Xi, H. Dependent ML, 1999. Available at http:\/\/www.cs.bu.edu\/~hwxi\/DML\/DML.html."},{"key":"5093031_CR26","unstructured":"Xi, H. Dependently typed data structures. In Proceedings of Workshop on Algorithmic Aspects of Advanced Programming Languages, Paris, France, 1999, pp. 17\u201333."},{"key":"5093031_CR27","unstructured":"Xi, H. Dependent types for program termination verification, 2000. Available as http:\/\/www.cs.bu.edu\/~hwxi\/DML\/Term."},{"key":"5093031_CR28","doi-asserted-by":"crossref","unstructured":"Xi, H. and Pfenning, F. Eliminating array bound checking through dependent types. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montr\u00e9al, Canada, 1998, pp. 249\u2013257.","DOI":"10.1145\/277650.277732"},{"key":"5093031_CR29","doi-asserted-by":"crossref","unstructured":"Xi, H. and Pfenning, F. Dependent types in practical programming. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, 1999, pp. 214\u2013227.","DOI":"10.1145\/292540.292560"},{"key":"5093031_CR30","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"Zantema, H. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24 (1995) 89\u2013105.","journal-title":"Fundamenta Informaticae"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1019916231463.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1019916231463\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1019916231463.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:52:02Z","timestamp":1751982722000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1019916231463"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["5093031"],"URL":"https:\/\/doi.org\/10.1023\/a:1019916231463","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}