{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:49Z","timestamp":1725664429981},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601647"},{"type":"electronic","value":"9783540446613"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60164-3_27","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:48:14Z","timestamp":1330278494000},"page":"182-199","source":"Crossref","is-referenced-by-count":33,"title":["Categorical reconstruction of a reduction free normalization proof"],"prefix":"10.1007","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Streicher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"12_CR1","unstructured":"Ulrich Berger. Personal email to Thomas Streicher, April 1994."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed \u03bb-calculus. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 202\u2013211, 1991.","DOI":"10.1109\/LICS.1991.151645"},{"key":"12_CR3","unstructured":"Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen (accepted for publication in Mathematical Structures in Computer Science), 1993."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Catarina Coquand. From Semantics to Rules: a Machine Assisted Analysis. In B\u00f6rger, Gurevich, and Meinke, editors, CSL'93, pages 91\u2013105. Springer-Verlag, LNCS 832, 1994.","DOI":"10.1007\/BFb0049326"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Neil Ghani. \u0392\u03b7-equality for coproducts. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, number 902 in LNCS, pages 171\u2013185, 1995.","DOI":"10.1007\/BFb0014052"},{"key":"12_CR7","unstructured":"G\u00e9rard Huet and Amokrane Sa\u00cfbi. Constructive category theory. In Peter Dybjer and Randy Pollack, editors, Informal proceedings of the joint CLICS-TYPES workshop on categories and type theory, 1995."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Saul A. Kripke. Semantical analysis of intutionistic logic I. In J.N. Crossley and M.A.E. Dummett, editors, Formal systems and recursive functions. North Holland, 1965.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"12_CR9","unstructured":"Joachim Lambek and Phil Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986."},{"key":"12_CR10","first-page":"73","volume-title":"Logic Colloquium 1973","author":"P. Martin-L\u00f6f","year":"1975","unstructured":"Per Martin-L\u00f6f. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73\u2013118, Amsterdam, 1975. North-Holland Publishing Company."},{"key":"12_CR11","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","volume":"51","author":"J. C. Mitchell","year":"1991","unstructured":"John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51:99\u2013124, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR12","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"12_CR13","unstructured":"A. S. Troelstra and D. van Dalen. Constructivism in Mathematics. An Introduction, volume II. North-Holland, 1988."}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60164-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:55:41Z","timestamp":1605646541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60164-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601647","9783540446613"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-60164-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}