{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:38:38Z","timestamp":1725493118434},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430308"},{"type":"electronic","value":"9783540453291"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45329-6_32","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T02:44:33Z","timestamp":1193366673000},"page":"321-334","source":"Crossref","is-referenced-by-count":0,"title":["A Context-Free Grammar Representation for Normal Inhabitants of Types in TA\u03bb"],"prefix":"10.1007","author":[{"given":"Sabine","family":"Broda","sequence":"first","affiliation":[]},{"given":"Lu\u00eds","family":"Damas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,23]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In Abramsky, Gabbay, and Maibaum, eds., Background: Computational Structures, volume 2 of Handbook of Logic in Computer Science, pp. 117\u2013309. Oxford Science Publications, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"32_CR2","unstructured":"C.-B. Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, Mathematics Dept., University of Wales Swansea, UK, 1979."},{"key":"32_CR3","first-page":"33","volume":"45","author":"S. Broda","year":"2001","unstructured":"S. Broda and L. Damas. Counting a type\u2019s (principal) inhabitants. Fundamenta Informaticae, 45:33\u201351, 2001.","journal-title":"Fundamenta Informaticae"},{"key":"32_CR4","unstructured":"S. Broda, and L. Damas. On the structure of normal \u03bb-terms having a certain type. Proceedings of 7th WoLLIC\u20192000, pp. 33\u201343, 2000."},{"key":"32_CR5","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0304-3975(99)00174-7","volume":"232","author":"M.W. Bunder","year":"2000","unstructured":"M.W. Bunder. Proof finding algorithms for implicational logics. Theoretical Computer Science, 232:165\u2013186, 2000.","journal-title":"Theoretical Computer Science"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"J. R. Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511608865"},{"key":"32_CR7","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/S0304-3975(97)00168-0","volume":"206","author":"S. Hirokawa","year":"1998","unstructured":"S. Hirokawa. Note: Infiniteness of proof(\u03b1) is polynomial-space complete. Theoretical Computer Science, 206:331\u2013339, 1998.","journal-title":"Theoretical Computer Science"},{"key":"32_CR8","unstructured":"W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, 1980."},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67\u201372, 1979.","journal-title":"Theoretical Computer Science"},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1006\/inco.1996.0027","volume":"125","author":"M. Takahashi","year":"1996","unstructured":"M. Takahashi, Y. Akama, and S. Hirokawa. Normal Proofs and Their Grammar. Information and Computation, 125:144\u2013153, 1996.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45329-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,18]],"date-time":"2024-02-18T17:43:34Z","timestamp":1708278214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45329-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430308","9783540453291"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45329-6_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}