{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:28:17Z","timestamp":1725535697932},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642031526"},{"type":"electronic","value":"9783642031533"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03153-3_3","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T06:11:14Z","timestamp":1248675074000},"page":"100-152","source":"Crossref","is-referenced-by-count":5,"title":["A Tutorial on Type-Based Termination"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Riba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1051\/ita:2004015","volume":"38","author":"A. Abel","year":"2004","unstructured":"Abel, A.: Termination Checking with Types. RAIRO \u2013 Theoretical Informatics and Applications\u00a038(4), 277\u2013319 (2004); Special Issue (FICS 2003)","journal-title":"RAIRO \u2013 Theoretical Informatics and Applications"},{"key":"3_CR2","unstructured":"Abel, A.: Type-Based Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, LMU University, Munich (2006)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Abel, A.: Semi-Continuous Sized Types and Termination. LMCS\u00a04(2-3) (2008)","DOI":"10.2168\/LMCS-4(2:3)2008"},{"key":"3_CR4","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of mathematical logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An Introduction to Inductive Definitions. In: Barwise, J. (ed.) Handbook of mathematical logic. Studies in Logic and the Foundations of Mathematics, vol.\u00a090, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-Based Termination of Recursive Definitions. Mathematical Structures in Computer Science\u00a014(1), 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11417170_7","volume-title":"Typed Lambda Calculi and Applications","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Gr\u00e9goire, B., Pastawski, F.: Practical Inference for Type-Based Termination in a Polymorphic Setting. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 71\u201385. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"W.-N. Chin","year":"2001","unstructured":"Chin, W.-N., Khoo, S.-C.: Calculating Sized Types. Higher-Order and Symbolic Computation\u00a014(2-3), 261\u2013300 (2001)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-58715-2_114","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Coquand","year":"1994","unstructured":"Coquand, T., Dybjer, P.: Inductive Definitions and Type Theory: an Introduction (Preliminary Version). In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol.\u00a0880, pp. 60\u201376. Springer, Heidelberg (1994)"},{"issue":"3","key":"3_CR9","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","volume":"53","author":"J.H. Gallier","year":"1991","unstructured":"Gallier, J.H.: What\u2019s So Special About Kruskal\u2019s Theorem and the Ordinal \u03930? A Survey of Some Results in Proof Theory. Annals of Pure and Applied Logic\u00a053(3), 199\u2013260 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E. Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural Recursive Definitions in Type Theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 397\u2013408. Springer, Heidelberg (1998)"},{"key":"3_CR11","unstructured":"Girard, J.-Y.: Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de l\u2019Arithm\u00e9tique d\u2019Ordre Sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris 7 (1972)"},{"key":"3_CR12","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., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)"},{"key":"3_CR13","first-page":"410","volume-title":"Proceedings of POPL 1996","author":"J. Hughes","year":"1996","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the Correctness of Reactive Systems Using Sized Types. In: Proceedings of POPL 1996, pp. 410\u2013423. ACM, New York (1996)"},{"key":"3_CR14","first-page":"30","volume-title":"Proceedings of LiCS 1987","author":"N.P. Mendler","year":"1987","unstructured":"Mendler, N.P.: Recursive Types and Type Constraints in Second Order Lambda-Calculus. In: Proceedings of LiCS 1987, pp. 30\u201336. IEEE Computer Society, Los Alamitos (1987)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-52753-2_47","volume-title":"CSL \u201989","author":"M. Parigot","year":"1990","unstructured":"Parigot, M.: On the Representation of Data in Lambda-Calculus. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1989. LNCS, vol.\u00a0440, pp. 309\u2013321. Springer, Heidelberg (1990)"},{"key":"3_CR16","first-page":"102","volume-title":"Proceedings of ICFP 1999","author":"Z. Sp\u0142awski","year":"1999","unstructured":"Sp\u0142awski, Z., Urzyczyn, P.: Type Fixpoints: Iteration vs. Recursion. In: Proceedings of ICFP 1999, pp. 102\u2013113. ACM, New York (1999)"},{"key":"3_CR17","unstructured":"Steffen, M.: Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen (1997)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/BFb0064875","volume-title":"Logic Colloquium","author":"W.W. Tait","year":"1975","unstructured":"Tait, W.W.: A Realizability Interpretation of the Theory of Species. In: Parikh, R. (ed.) Logic Colloquium. LNCS, vol.\u00a0453, pp. 240\u2013251. Springer, Heidelberg (1975)"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H. Xi","year":"2002","unstructured":"Xi, H.: Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation\u00a015(1), 91\u2013131 (2002)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Language Engineering and Rigorous Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03153-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T18:08:27Z","timestamp":1558462107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03153-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642031526","9783642031533"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03153-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}