{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:27Z","timestamp":1725663987485},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578871"},{"type":"electronic","value":"9783540483830"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57887-0_111","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:37:45Z","timestamp":1330263465000},"page":"465-493","source":"Crossref","is-referenced-by-count":2,"title":["Normal proofs and their grammar"],"prefix":"10.1007","author":[{"given":"M.","family":"Takahashi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Akama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Hirokawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"25_CR1","unstructured":"Y. Akama. Number of proofs and tree automaton. manuscript, 1991."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"H Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbai, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"25_CR3","unstructured":"S. Berardi. Personal communication, 1993."},{"key":"25_CR4","volume-title":"PhD thesis","author":"C.-B. Ben-Yelles","year":"1979","unstructured":"C.-B. Ben-Yelles. Type-assignment in the Lambda-calculus. PhD thesis, University College, Swansea, 1979."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"H. Geuvers. Conservativity between logics and typed \u03bb calculi. In H. Geuvers, editor, Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pages 131\u2013156, 1993.","DOI":"10.1007\/3-540-58085-9_73"},{"issue":"2","key":"25_CR6","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.J. Nederhof. Modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, 1(2):155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"25_CR7","unstructured":"J.R Hindley. The Simple Theory of Type Assignment. Forthcoming."},{"key":"25_CR8","unstructured":"S. Hirokawa. The number of proofs for implicational formulas(abstract). In Proceedings of Logic Colloquium '92, volume 36. Janos Bolyai Mathematical Society, 1992."},{"key":"25_CR9","unstructured":"J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979."},{"issue":"4","key":"25_CR10","doi-asserted-by":"crossref","first-page":"705","DOI":"10.2307\/2272390","volume":"41","author":"M. L\u00f6b","year":"1976","unstructured":"M. L\u00f6b. Embedding first order predicate logic in fragments of intuitionistic logic. Journal of Symbolic Logic, 41(4):705\u2013718, 1976.","journal-title":"Journal of Symbolic Logic"},{"key":"25_CR11","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction. Almqvist and Wiksell, 1965. Stockholm."},{"key":"25_CR12","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L.S. Benthem van","year":"1993","unstructured":"L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105:30\u201341, 1993.","journal-title":"Information and Computation"},{"key":"25_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90077-6","volume":"52","author":"M. Zaionc","year":"1987","unstructured":"M. Zaionc. Word operation definable in the typed \u03bb-calculus. Theoretical computer science, 52:1\u201314, 1987.","journal-title":"Theoretical computer science"},{"key":"25_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0168-0072(91)90019-I","volume":"51","author":"M. Zaionc","year":"1991","unstructured":"M. Zaionc. \u03bb-definability on free algebras. Annals of Pure and Applied Logic, 51:279\u2013300, 1991.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57887-0_111.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:37:16Z","timestamp":1713627436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57887-0_111"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578871","9783540483830"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-57887-0_111","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}