{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:17:05Z","timestamp":1778757425357,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540590484","type":"print"},{"value":"9783540491781","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014068","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"414-427","source":"Crossref","is-referenced-by-count":12,"title":["Categorical completeness results for the simply-typed lambda-calculus"],"prefix":"10.1007","author":[{"given":"Alex K.","family":"Simpson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"28_CR1","unstructured":"Y. Akama. On Mints' reduction for ccc-calculus. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, Proceedings of TLCA '93. LNCS 664, Springer Verlag, 1993."},{"key":"28_CR2","volume-title":"The Lambda Calculus, its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 1984. Second edition.","edition":"Second edition"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed \u03bb-calculus. In Proceedings of 6th Annual Symposium on Logic in Computer Science, pages 203\u2013211, 1991.","DOI":"10.1109\/LICS.1991.151645"},{"key":"28_CR4","unstructured":"D. \u010cubri\u0107. Embedding of a free cartesian closed category into the category of sets. Journal of Pure and Applied Algebra, to appear, 1995."},{"key":"28_CR5","volume-title":"Logic Colloquium","author":"H. Friedman","year":"1975","unstructured":"H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium, Springer-Verlag, New York, 1975."},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"N. Ghani. \u03b2\u03b7-equality for coproducts. This volume, 1995.","DOI":"10.1007\/BFb0014052"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"C. B. Jay and N. Ghani. The virtues of eta-expansion. Journal of Functional Programming, to appear, 1995.","DOI":"10.1017\/S0956796800001301"},{"key":"28_CR8","unstructured":"J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986."},{"key":"28_CR9","unstructured":"E. Moggi. The Partial Lambda-Calculus. Ph.D. thesis, Department of Computer Science, University of Edinburgh, 1988. Available as LFCS report no. ECS-LFCS-88-63."},{"key":"28_CR10","unstructured":"G. D. Plotkin. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, 1973."},{"key":"28_CR11","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G. D. Plotkin","year":"1980","unstructured":"G. D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980."},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"J. G. Riecke. Statman's 1-Section Theorem. Information and Computation, to appear, 1995.","DOI":"10.1006\/inco.1995.1021"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"1387","DOI":"10.1007\/BF01084396","volume":"22","author":"S. Soloviev","year":"1983","unstructured":"S. Soloviev. The category of finite sets and CCCs. Journal of Soviet Mathematics, 22:1387\u20131400, 1983.","journal-title":"Journal of Soviet Mathematics"},{"key":"28_CR14","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"R. Statman","year":"1980","unstructured":"R. Statman. On the existence of closed terms in the typed \u03bb-calculus I. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980."},{"key":"28_CR15","doi-asserted-by":"crossref","first-page":"17","DOI":"10.2307\/2273377","volume":"47","author":"R. Statman","year":"1982","unstructured":"R. Statman. Completeness, invariance and \u03bb-definability. Journal of Symbolic Logic, 47:17\u201326, 1982.","journal-title":"Journal of Symbolic Logic"},{"key":"28_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF02023009","volume":"23","author":"R. Statman","year":"1983","unstructured":"R. Statman. \u03bb-definable functionals and \u03b2\u03b7 conversion. Archiv fur Math. Logik und Grund., 23:21\u201326, 1983.","journal-title":"Archiv fur Math. Logik und Grund."},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"R. Statman. Equality between functionals revisited. In L. A. Harrington et al, editors, Harvey Friedman's Research on the Foundations of Mathematics. Elsevier Science Publishers, 1985.","DOI":"10.1016\/S0049-237X(09)70166-1"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014068","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:38:01Z","timestamp":1586579881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014068"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0014068","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}