{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:27:00Z","timestamp":1725460020690},"publisher-location":"Boston","reference-count":13,"publisher":"Kluwer Academic Publishers","isbn-type":[{"type":"print","value":"1402081405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_48","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"633-646","source":"Crossref","is-referenced-by-count":1,"title":["The Simply-Typed Pure Pattern Type System Ensures Strong Normalization"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Wack","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"48_CR1","doi-asserted-by":"crossref","unstructured":"Barendregt, H. P.(1992).Lambda calculi with types. In Abramsky, S., Gabbay, D., and Maibaum, T., editors, Handbook of Logic in Computer Science. Clarendon Press.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"48_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., and Liquori, L.(2003). Pure Patterns Type Systems. In POPL 2003, New Orleans, USA. ACM.","DOI":"10.1145\/604131.604152"},{"key":"48_CR3","doi-asserted-by":"crossref","unstructured":"Blanqui, F. (2001). Definitions by rewriting in the calculus of constructions. In LICS, pages 9\u201318.","DOI":"10.1109\/LICS.2001.932478"},{"key":"48_CR4","unstructured":"Cirstea, H. and Kirchner, C. (2000). The typed rewriting calculus. In Third International Workshop on Rewriting Logic and Application, Kanazawa (Japan)."},{"key":"48_CR5","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C., and Liquori, L. (2001). The Rho Cube. In Honsell, F., editor, FOSSACS, volume 2030 of LNCS, pages 166\u2013180, Genova, Italy.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"48_CR6","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Liquori, L., and Wack, B.(2004). Rewriting calculus with fixpoints: Untyped and first-order systems. In TYPES\u201903, LNCS, Torino.To be published.","DOI":"10.1007\/978-3-540-24849-1_10"},{"key":"48_CR7","unstructured":"Coquand, T.(1992). Pattern matching with dependent types. In Informal proceedings workshop on types for proofs and programs, pages 71\u201384. B\u00e5stad, Su\u00e8de."},{"key":"48_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and Huet, G.(1988). The calculus of constructions. Information and Computation, 76:95\u2013120.","journal-title":"Information and Computation"},{"key":"48_CR9","unstructured":"Dowek, G., Hardin, T., and Kirchner, C.(2003). Theorem proving modulo, revised version. Rapport de Recherche 4861, INRIA."},{"key":"48_CR10","unstructured":"Girard, J.-Y.(1972). Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithmetique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII."},{"issue":"1","key":"48_CR11","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1006\/inco.1996.0004","volume":"124","author":"D. Kesner","year":"1996","unstructured":"Kesner, D., Puel, L., and Tannen, V.(1996). A typed pattern calculus. Information and Computation, 124(1):32\u201361.","journal-title":"Information and Computation"},{"key":"48_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. Klop","year":"1993","unstructured":"Klop, J., van Oostrom, V., and van Raamsdonk, F. (1993). Combinatory reduction systems: introduction and survey. TCS, 121:279\u2013308.","journal-title":"TCS"},{"key":"48_CR13","unstructured":"Werner, B.(1994). Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII."}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,3]],"date-time":"2024-02-03T01:34:46Z","timestamp":1706924086000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_48","relation":{},"subject":[]}}