{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:55Z","timestamp":1749125155611},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014051","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:50:31Z","timestamp":1132714231000},"page":"154-170","source":"Crossref","is-referenced-by-count":6,"title":["Lambda-calculus, combinators and the comprehension scheme"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"crossref","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"P.B. Andrews, General models, descriptions and choice in type theory, The Journal of Symbolic Logic, 37, 2 (1972) pp. 385\u2013394.","journal-title":"The Journal of Symbolic Logic"},{"key":"11_CR2","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"P.B. Andrews","year":"1986","unstructured":"P.B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press, Orlando (1986)."},{"key":"11_CR3","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, 5 (1940), pp. 56\u201368.","journal-title":"The Journal of Symbolic Logic"},{"key":"11_CR4","doi-asserted-by":"crossref","first-page":"363","DOI":"10.2307\/2370728","volume":"51","author":"H. Curry","year":"1929","unstructured":"H. Curry, An analysis of logical substitution, American Journal of Mathematics, 51 (1929), pp. 363\u2013384.","journal-title":"American Journal of Mathematics"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"G. Dowek, Lambda-calculus, combinators and the comprehension scheme, manuscript (1994).","DOI":"10.1007\/BFb0014051"},{"key":"11_CR6","unstructured":"G. Dowek, Collections, types and sets, manuscript (1994)."},{"key":"11_CR7","unstructured":"J.Y. Girard, Y. Lafont, P. Taylor, Types and proofs, Cambridge University Press (1989)."},{"issue":"3","key":"11_CR8","doi-asserted-by":"crossref","first-page":"201","DOI":"10.2307\/2267403","volume":"18","author":"L. Henkin","year":"1953","unstructured":"L. Henkin, Banishing the rule of substitution for functional variables, The Journal of Symbolic Logic, 18, 3 (1953), pp. 201\u2013208.","journal-title":"The Journal of Symbolic Logic"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"R.J.M. Hughes, Super-combinators, a new implementation method for applicative languages, Proceedings of Lisp and Functional Programming (1982).","DOI":"10.1145\/800068.802129"},{"key":"11_CR10","unstructured":"D.A. Miller, Proofs in higher order logic, PhD Thesis, Carnegie Mellon University (1983)."},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/BF00370646","volume":"46","author":"D.A. Miller","year":"1987","unstructured":"D.A. Miller, A compact representation of proofs, Studia Logica, 46, 4 (1987).","journal-title":"Studia Logica"},{"key":"11_CR12","first-page":"125","volume":"10","author":"T. Skolem","year":"1928","unstructured":"T. Skolem, \u00dcber die mathematische logik, Norsk Matematisk Tidsskrift, 10 (1928), pp. 125\u2013142.","journal-title":"Norsk Matematisk Tidsskrift"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:37:29Z","timestamp":1586565449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0014051","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}