{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:17:47Z","timestamp":1742617067347,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_68","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:47:27Z","timestamp":1330210047000},"page":"633-650","source":"Crossref","is-referenced-by-count":1,"title":["Principal type-schemes of BCI-lambda-terms"],"prefix":"10.1007","author":[{"given":"Sachio","family":"Hirokawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"31_CR1","first-page":"3","volume":"88","author":"A.A. Babaev","year":"1979","unstructured":"A.A. Babaev, S.V. Solov'ev. A coherence theorem for canonical morphism in cartesian closed categories. Zapiski nauchnykh Seminarov Lenigradskogo Otdeleniya matematichskogo Instituta im. V.A. Steklova An SSSR 88:3\u201329, 1979.","journal-title":"Zapiski nauchnykh Seminarov Lenigradskogo Otdeleniya matematichskogo Instituta im. V.A. Steklova An SSSR"},{"key":"31_CR2","volume-title":"Type-assignment in the lambda-calculus","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":"31_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. Theoret. Comput. Sci. 50:1\u2013101, 1987.","journal-title":"Theoret. Comput. Sci."},{"key":"31_CR4","first-page":"29","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"J.R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146:29\u201360 1969.","journal-title":"Trans. Amer. Math. Soc."},{"key":"31_CR5","volume-title":"Introduction to Combinators and Lambda-Calculus","author":"J. R. Hindley","year":"1986","unstructured":"J. R. Hindley and J. P Seldin. Introduction to Combinators and Lambda-Calculus. Cambridge Univ. Press, London, 1986."},{"key":"31_CR6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(89)90100-X","volume":"64","author":"J. R. Hindley","year":"1989","unstructured":"J. R. Hindley. BCK-combinators and linear lambda-terms have types. Theoret. Comp. Sci. 64:97\u2013105, 1989.","journal-title":"Theoret. Comp. Sci."},{"key":"31_CR7","unstructured":"J. R. Hindley. The Meyer-Bunder theorem: Every inhabited type is a P.T.S. in BB'IW-combinatory logic. Manuscript 1989."},{"key":"31_CR8","doi-asserted-by":"crossref","first-page":"90","DOI":"10.2307\/2274956","volume":"50","author":"J. R. Hindley","year":"1990","unstructured":"J. R. Hindley and D. Meredith. Principal type-schemes and condensed detachment. J. Symbolic Logic 50:90\u2013105, 1990.","journal-title":"J. Symbolic Logic"},{"key":"31_CR9","unstructured":"J. R. Hindley. BCK and BCI logics, condensed detachment and the 2-property, a summary. Report, Univ. of Wolongon, Aug 1990."},{"key":"31_CR10","unstructured":"S. Hirokawa. Principal types of BCK-lambda terms. submitted."},{"key":"31_CR11","unstructured":"S. Hirokawa. Principal type assignment to lambda terms. submitted."},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"S. Hirokawa. Converse principal-type-scheme theorem in lambda-calculus. Studia Logica (to appear).","DOI":"10.1007\/BF00370332"},{"key":"31_CR13","unstructured":"W. A. Howard. The formulae-as-types notion of construction. In J. R. Hindley and J. P Seldin, editors, To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"31_CR14","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1002\/malq.19630091206","volume":"9","author":"S. Jaskowski","year":"1963","unstructured":"S. Jaskowski. \u00dcber Tautologien, in welchen keine Variable merh Als zweimal vorkommt. Zeitschrift f\u00fcr Math. Logik 9:219\u2013228, 1963.","journal-title":"Zeitschrift f\u00fcr Math. Logik"},{"key":"31_CR15","unstructured":"Y. Komori. BCK algebras and lambda calculus. In Proceedings of 10th Symp. on Semigroups, Sakado 1986, pages 5\u201311. Josai University, 1987."},{"key":"31_CR16","unstructured":"R. K. Meyer and M. W. Bunder. Condensed detachment and combinators. J. Automated Reasoning (to appear)."},{"key":"31_CR17","unstructured":"G. E. Mints. A simple proof of the coherence theorem for cartesian closed categories. Manuscript 1982."},{"key":"31_CR18","unstructured":"G. E. Mints and T. Tammet. Condensed detachment is complete for relevant logic: proof using computer. J. Automated Reasoning (to appear)."}],"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-54415-1_68.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:18:20Z","timestamp":1742591900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_68"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_68","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}