{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:32Z","timestamp":1767927692916,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540626886","type":"print"},{"value":"9783540684381","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_47","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:34Z","timestamp":1330296514000},"page":"373-389","source":"Crossref","is-referenced-by-count":21,"title":["Inhabitation in typed lambda-calculi (a syntactic approach)"],"prefix":"10.1007","author":[{"given":"Pawel","family":"Urzyczyn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"23_CR1","unstructured":"Arts, T., Embedding first order predicate logic in second order prepositional logic, Master Thesis, Katholieke Universiteit Nijmegen, 1992."},{"key":"23_CR2","unstructured":"Arts, T., Dekkers, W., Embedding first order predicate logic in second order propositional logic, Technical report 93-02, Katholieke Universiteit Nijmegen, 1993."},{"key":"23_CR3","unstructured":"Barendregt, H.P., Lambda calculi with types, chapter in: Handbook of Logic in Computer Science (S. Abramsky, D.M. Gabbay, T. Maibaum eds.), Oxford University Press, 1990, pp. 117\u2013309."},{"key":"23_CR4","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/BF02015377","volume":"16","author":"D.M. Gabbay","year":"1974","unstructured":"Gabbay, D.M., On 2nd order intuitionistic propositional calculus with full comprehension, Arch. math. Logik, 16 (1974), 177\u2013186.","journal-title":"Arch. math. Logik"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Semantical Investigations in Heyting's Intuitionistic Logic, D. Reidel Publ. Co., 1981.","DOI":"10.1007\/978-94-017-2977-2"},{"key":"23_CR6","volume-title":"Cambridge Tracts in Theoretical Computer Science 7","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, Cambridge, 1989."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Leivant, D., Polymorphic type inference, Proc. 10-th ACM Symposium on Principles of Programming Languages, ACM, 1983.","DOI":"10.1145\/567067.567077"},{"issue":"No.4","key":"23_CR8","doi-asserted-by":"crossref","first-page":"705","DOI":"10.2307\/2272390","volume":"41","author":"M. H. L\u00f6b","year":"1976","unstructured":"L\u00f6b, M. H., Embedding first order predicate logic in fragments of intuitionistic logic, Journal Symb. Logic, 41, No. 4 (1976), 705\u2013718.","journal-title":"Journal Symb. Logic"},{"key":"23_CR9","first-page":"259","volume-title":"Intuitionism and Proof Theory","author":"D. Prawitz","year":"1970","unstructured":"Prawitz, D., Some results for intuitionistic logic with second order quantification rules, in: Intuitionism and Proof Theory (A. Kino, J. Myhill, R.E. Vesley eds.), North-Holland, Amsterdam, 1970, pp. 259\u2013270."},{"key":"23_CR10","volume-title":"The Mathematics of Metamathematics","author":"H. Rasiowa","year":"1963","unstructured":"Rasiowa, H., Sikorski, R., The Mathematics of Metamathematics, PWN, Warsaw, 1963."},{"key":"23_CR11","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoretical Computer Science\n9, 67\u201372 (1979)","journal-title":"Theoretical Computer Science"},{"key":"23_CR12","series-title":"LNCS 664","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/BFb0037122","volume-title":"Mathematical Structures in Computer Science. Preliminary version in Proc. Typed Lambda Calculus and Applications","author":"P. Urzyczyn","year":"1993","unstructured":"Urzyczyn, P., Type reconstruction in F\u03c9, to appear in Mathematical Structures in Computer Science. Preliminary version in Proc. Typed Lambda Calculus and Applications (M. Bezem and J.F. Groote, eds.), LNCS 664, Springer-Verlag, Berlin, 1993, pp. 418\u2013432."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Urzyczyn, P., The emptiness problem for intersection types, Proc. 9th IEEE Symposium on Logic in Computer Science, 1994, pp. 300\u2013309. (To appear in Journal of Symbolic Logic.)","DOI":"10.1109\/LICS.1994.316059"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Wells, J.B., Typability and type checking in the second-order \u03bb-calculus calculus are equivalent and undecidable, Proc. 9th IEEE Symposium on Logic in Computer Science, 1994, pp. 176\u2013185. (To appear in Annals of Pure and Applied Logic.)","DOI":"10.1109\/LICS.1994.316068"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:39:35Z","timestamp":1619573975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}