{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:30Z","timestamp":1746745470455},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_24","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"333-347","source":"Crossref","is-referenced-by-count":7,"title":["On Strong Normalization of the Calculus of Constructions with Type-Based Termination"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"first","affiliation":[]},{"given":"Jorge Luis","family":"Sacchini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Abel, A.: A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (2006)"},{"key":"24_CR2","unstructured":"Altenkirch, T.: Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh (November 1993)"},{"key":"24_CR3","unstructured":"Barras, B.: Sets in coq, coq in sets. In: 1st Coq Workshop (August 2009)"},{"key":"24_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11916277_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Pastawski, F.: CIC $\\widehat{~}$ : Type-based termination of recursive definitions in the Calculus of Inductive Constructions. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 257\u2013271. Springer, Heidelberg (2006)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2004","unstructured":"Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 24\u201339. Springer, Heidelberg (2004)"},{"key":"24_CR6","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":"24_CR7","doi-asserted-by":"crossref","unstructured":"Grgoire, B., Sacchini, J.L.: On strong normalization of the Calculus of Constructions with type-based termination (2010), http:\/\/www-sop.inria.fr\/members\/Jorge-Luis.Sacchini\/papers\/sn.pdf","DOI":"10.1007\/978-3-642-16242-8_24"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL, pp. 410\u2013423 (1996)","DOI":"10.1145\/237721.240882"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"24_CR10","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and reasoning: a type theory for computer science","author":"Z. Luo","year":"1994","unstructured":"Luo, Z.: Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., New York (1994)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/BFb0097796","volume-title":"Types for Proofs and Programs","author":"P.-A. Melli\u00e8s","year":"1998","unstructured":"Melli\u00e8s, P.-A., Werner, B.: A generic normalisation proof for pure type systems. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 254\u2013276. Springer, Heidelberg (1998)"},{"key":"24_CR12","unstructured":"Wahlstedt, D.: Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion. PhD thesis, Chalmers University of Technology (2007) ISBN 978-91-7291-979-2"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,30]],"date-time":"2024-03-30T22:24:06Z","timestamp":1711837446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}