{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:58:18Z","timestamp":1715061498852},"reference-count":51,"publisher":"EDP Sciences","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"published-print":{"date-parts":[[2004,10]]},"DOI":"10.1051\/ita:2004015","type":"journal-article","created":{"date-parts":[[2008,9,12]],"date-time":"2008-09-12T08:27:30Z","timestamp":1221208050000},"page":"277-319","source":"Crossref","is-referenced-by-count":25,"title":["Termination checking with types"],"prefix":"10.1051","volume":"38","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]}],"member":"250","published-online":{"date-parts":[[2004,10,15]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44557-9_1","volume":"1956","author":"Abel","year":"2000","journal-title":"Lect. Notes Comput. Sci."},{"key":"R2","unstructured":"A. Abel, A third-order representation of the\u03bb\u00b5-calculus, edited by S. Ambler, R. Crole, A. Momigliano, Elsevier Science Publishers.Electron. Notes Theor. Comput. Sci.58(2001)."},{"key":"R3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44904-3_1","volume":"2701","author":"Abel","year":"2003","journal-title":"Lect. Notes Comput. Sci."},{"key":"R4","unstructured":"A. Abel,Soundness of a bidirectional typing algorithm. Twelf code, available on the author's homepage, http:\/\/www.tcs.informatik.uni-muenchen.de\/\u00a0abel (May 2004)."},{"key":"R5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"Abel","year":"2002","journal-title":"J. Funct. Programming"},{"key":"R6","unstructured":"T. Altenkirch,Constructions, Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh (Nov. 1993)."},{"key":"R7","doi-asserted-by":"crossref","unstructured":"R.M. Amadio and S. Coupet-Grimal, Analysis of a guard condition in type theory, inFoundations of Software Science and Computation Structures, First International Conference, FoSSaCS'98, edited by M. Nivat, Springer.Lect. Notes Comput. Sci.1378(1998).","DOI":"10.1007\/BFb0053541"},{"key":"R8","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"Arts","year":"2000","journal-title":"Theor. Comput. Sci."},{"key":"R9","unstructured":"G. Barthe, M.J. Frade, E. Gim\u00e9nez, L. Pinto and T. Uustalu, Type-based termination of recursive definitions.Math. Struct. Comput. Sci.14(2004) 1\u201345."},{"key":"R10","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/BFb0055783","volume":"1450","author":"Bierman","year":"1998","journal-title":"Lect. Notes Comput. Sci."},{"key":"R11","unstructured":"F. Blanqui,Type Theory and Rewriting. Ph.D. Thesis, Universit\u00e9 Paris XI (Sept. 2001)."},{"key":"R12","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","volume":"3091","author":"Blanqui","year":"2004","journal-title":"Lect. Notes Comput. Sci."},{"key":"R13","unstructured":"F. Blanqui, J.-P. Jouannaud and M. Okada, Inductive data type systems.Theor. Comput. Sci.277(2001)."},{"key":"R14","doi-asserted-by":"crossref","unstructured":"J. Brauburger and J. Giesl, Termination analysis for partial functions, inProc. of the Third International Static Analysis Symposium (SAS'96), Aachen, Germany, Springer.Lect. Notes Comput. Sci.1145(1996).","DOI":"10.1007\/3-540-61739-6_37"},{"key":"R15","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"Chin","year":"2001","journal-title":"Higher-Order and Symbolic Computation"},{"key":"R16","unstructured":"C. Coquand, Agda. WWW page (2000) http:\/\/www.cs.chalmers.se\/\u00a0catarina\/agda\/"},{"key":"R17","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume":"806","author":"Coquand","year":"1993","journal-title":"Lect. Notes Comput. Sci."},{"key":"R18","unstructured":"T. Coquand, An algorithm for type-checking dependent types, inMathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction, July 17\u201321, 1995, Kloster Irsee, Germany, Elsevier Science.Sci. Comput. Programming26167\u2013177 (1996)."},{"key":"R19","doi-asserted-by":"crossref","unstructured":"K. Crary and S. Weirich, Resource bound certification, inProc. of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA (Jan. 2000) 184\u2013198.","DOI":"10.1145\/325694.325716"},{"key":"R20","doi-asserted-by":"crossref","unstructured":"R. Davies and F. Pfenning, Intersection types and computational effects, inProc. of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada (Sept. 2000) 198\u2013208.","DOI":"10.1145\/351240.351259"},{"key":"R21","doi-asserted-by":"crossref","unstructured":"J. Dunfield and F. Pfenning, Tridirectional typechecking, in31st Annual Symposium on Principles of Programming Languages (POPL'04), edited by N.D. Jones and X. Leroy, Venice, Italy. ACM (Jan. 2004) 281\u2013292.","DOI":"10.1145\/964001.964025"},{"key":"R22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"Giesl","year":"1997","journal-title":"J. Automat. Reason."},{"key":"R23","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BFb0055070","volume":"1443","author":"Gim\u00e9nez","year":"1998","journal-title":"Lect. Notes Comput. Sci."},{"key":"R24","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-36575-3_20","volume":"2618","author":"Haack","year":"2003","journal-title":"Lect. Notes Comput. Sci."},{"key":"R25","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/3-540-18508-9_24","volume":"283","author":"Hagino","year":"1987","journal-title":"Lect. Notes Comput. Sci."},{"key":"R26","unstructured":"T. Hallgren, Alfa home page. http:\/\/www.math.chalmers.se\/\u00a0hallgren\/Alfa\/ (2003)."},{"key":"R27","doi-asserted-by":"crossref","unstructured":"J. Hughes and L. Pareto, Recursion and dynamic data-structures in bounded space: Towards embedded ML programming, inInternational Conference on Functional Programming (ICFP'99)(1999) 70\u201381.","DOI":"10.1145\/317636.317785"},{"key":"R28","doi-asserted-by":"crossref","unstructured":"J. Hughes, L. Pareto and A. Sabry, Proving the correctness of reactive systems using sized types, inSymposium on Principles of Programming Languages(1996) 410\u2013423.","DOI":"10.1145\/237721.240882"},{"key":"R29","unstructured":"INRIA,The Coq Proof Assistant Reference Manual, version 8.0 edition (April 2004). http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"R30","doi-asserted-by":"crossref","unstructured":"C.S. Lee, N.D. Jones and A.M. Ben-Amram, The size-change principle for program termination, inACM Symposium on Principles of Programming Languages (POPL'01), London, UK. ACM Press (Jan. 2001).","DOI":"10.1145\/360204.360210"},{"key":"R31","unstructured":"Z. Luo,ECC: An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh (1990)."},{"key":"R32","unstructured":"R. Matthes,Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. Thesis, Ludwig-Maximilians-University (May 1998)."},{"key":"R33","unstructured":"C. McBride,Dependently Typed Functional Programs and their Proofs. Ph.D. Thesis, University of Edinburgh (1999)."},{"key":"R34","unstructured":"N.P. Mendler, Recursive types and type constraints in second-order lambda calculus, inProc. of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, New York. IEEE Computer Society Press (1987) 30\u201336."},{"key":"R35","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"Mendler","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"R36","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"Milner","year":"1978","journal-title":"J. Comput. Syst. Sci."},{"key":"R37","unstructured":"L. Pareto,Types for Crash Prevention. Ph.D. Thesis, Chalmers University of Technology (2000)."},{"key":"R38","unstructured":"M. Parigot,\u03bb\u00b5-calculus: An algorithmic interpretation of classical natural deduction, inLogic Programming and Automated Reasoning: Proc.\u2000of the International Conference LPAR'92, edited by A. Voronkov, Springer, Berlin, Heidelberg (1992) 190\u2013201."},{"key":"R39","first-page":"202","volume":"1632","author":"Pfenning","year":"1999","journal-title":"Lect. Notes Artif. Intell."},{"key":"R40","first-page":"401","volume":"2083","author":"Pientka","year":"2001","journal-title":"Lect. Notes Artif. Intell."},{"key":"R41","unstructured":"B.C. Pierce,Types and Programming Languages. MIT Press (2002)."},{"key":"R42","unstructured":"B.C. Pierce, D.N. Turner, Local type inference, inPOPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California (1998)."},{"key":"R43","unstructured":"R. Pollack,The Theory of LEGO. Ph.D. Thesis, University of Edinburgh (1994)."},{"key":"R44","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/317765.317789","volume":"34","author":"Sp\u0142awski","year":"1999","journal-title":"SIGPLAN Notices"},{"key":"R45","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/BFb0000493","volume":"1349","author":"Telford","year":"1997","journal-title":"Lect. Notes Comput. Sci."},{"key":"R46","first-page":"474","volume":"6","author":"Telford","year":"2000","journal-title":"J. Universal Comput. Sci."},{"key":"R47","first-page":"5","volume":"10","author":"Uustalu","year":"1999","journal-title":"Informatica (Lithuanian Academy of Sciences)"},{"key":"R48","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1007\/BFb0012861","volume":"310","author":"Walther","year":"1988","journal-title":"Lect. Notes Comput. Sci."},{"key":"R49","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"Wright","year":"1994","journal-title":"Inform. Comput."},{"key":"R50","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"Dependent","year":"2002","journal-title":"J. Higher-Order and Symbolic Computation"},{"key":"R51","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1093\/comjnl\/45.4.436","volume":"45","author":"Yang","year":"2002","journal-title":"Comput. J."}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita:2004015\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T22:54:13Z","timestamp":1684536853000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita:2004015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10]]},"references-count":51,"journal-issue":{"issue":"4"},"alternative-id":["ita0428NS"],"URL":"https:\/\/doi.org\/10.1051\/ita:2004015","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"value":"0988-3754","type":"print"},{"value":"1290-385X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,10]]}}}