{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:44Z","timestamp":1761611204900},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657637"},{"type":"electronic","value":"9783540489597"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48959-2_7","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T12:52:16Z","timestamp":1178196736000},"page":"69-82","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Counting a Type\u2019s Principal Inhabitants"],"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,5,27]]},"reference":[{"key":"7_CR1","unstructured":"H. Barendregt. Lambda calculi with types. In Abramsky, Gabbay, and Maibaum, editors, Background: Computational Structures, volume 2 of Handbook of Logic in Computer Science, pages 117\u2013309. Oxford Science Publications, 1992."},{"key":"7_CR2","volume-title":"Type-assignment in the lambda-calculus; syntax and semantics","author":"C.-B. Ben-Yelles","year":"1979","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":"7_CR3","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":"7_CR4","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(93)90171-O","volume":"107","author":"S. Hirokawa","year":"1993","unstructured":"S. Hirokawa. Principal types of BCK-lambda-terms. Theoretical Computer Science, 107:253\u2013276, 1993.","journal-title":"Theoretical Computer Science"},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-57887-0_111","volume-title":"Theoretical Aspects of Computer Software (TACS\u201994)","author":"M. Takahashi","year":"1994","unstructured":"M. Takahashi, Y. Akama, and S. Hirokawa. Normal proofs and their grammar. In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software (TACS\u201994), volume 789 of LNCS, pages 465\u2013493. Springer Verlag, 1994."},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-15976-2_23","volume-title":"Rewriting Techniques and Applications","author":"M. Zaionc","year":"1985","unstructured":"M. Zaionc. The set of unifiers in typed \u03bb-calculus as regular expression. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, volume 202 of LNCS, pages 430\u2013440. Springer Verlag, 1985."},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00244393","volume":"4","author":"M. Zaionc","year":"1988","unstructured":"M. Zaionc. Mechanical procedure for proof construction via closed terms in typed \u03bb-calculus. J. Automated Reasoning, 4:173\u2013190, 1988.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48959-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:07:53Z","timestamp":1558256873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48959-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657637","9783540489597"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-48959-2_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"27 May 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}