{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:11:55Z","timestamp":1747807915868},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642031526"},{"type":"electronic","value":"9783642031533"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03153-3_1","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T06:11:14Z","timestamp":1248675074000},"page":"1-56","source":"Crossref","is-referenced-by-count":4,"title":["Introduction to Type Theory"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E.S. Bainbridge","year":"1990","unstructured":"Bainbridge, E.S., Freyd, P.J., Scedrov, A., Scott, P.J.: Functorial polymorphism. Theoretical Computer Science\u00a070, 35\u201364 (1990)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"1_CR2","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/S0168-0072(96)00036-X","volume":"86","author":"S. Bakel van","year":"1997","unstructured":"van Bakel, S., Liquori, L., Ronchi Della Rocca, S., Urzyczyn, P.: Comparing Cubes of Typed and Type Assignment Systems. Ann. Pure Appl. Logic\u00a086(3), 267\u2013303 (1997)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. Barendregt","year":"1981","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North Holland, Amsterdam (1981)"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"1149","DOI":"10.1016\/B978-044450813-3\/50020-5","volume-title":"Handbook of Automated Reasoning, ch.18","author":"H. Barendregt","year":"2001","unstructured":"Barendregt, H., Geuvers, H.: Proof Assistants using Dependent Type Systems. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch.18, vol.\u00a02, pp. 1149\u20131238. Elsevier, Amsterdam (2001)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Lambda Calculi with Types. In: Abramsky, Gabbay, Maibaum (eds.) Handbook of Logic in Computer Science, vol.\u00a01. Clarendon (1992)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"1_CR6","series-title":"EATCS Series: Texts in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art : the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions. EATCS Series: Texts in Theoretical Computer Science, 469 p. Springer, Heidelberg (2004)"},{"issue":"5","key":"1_CR7","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1017\/S0956796800001969","volume":"6","author":"M. Bezem","year":"1996","unstructured":"Bezem, M., Springintveld, J.: A Simple Proof of the Undecidability of Inhabitation in \u03bbP. J. Funct. Program.\u00a06(5), 757\u2013761 (1996)","journal-title":"J. Funct. Program."},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"B\u00f6hm, C., Berarducci, A.: Automatic synthesis of typed \u03bb-programs on term algebras. Theoretical Computer Science\u00a039, 135\u2013154 (1985)","journal-title":"Theoretical Computer Science"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR10","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ (1986)"},{"key":"1_CR11","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B., Feys, R., Craig, W.: Combinatory Logic, vol.\u00a01. North\u2013Holland, Amsterdam (1958)"},{"key":"1_CR12","first-page":"207","volume-title":"POPL 1982: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"L. Damas","year":"1982","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL 1982: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 207\u2013212. ACM, New York (1982)"},{"volume-title":"The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions","year":"1965","key":"1_CR13","unstructured":"Davis, M. (ed.): The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. Raven Press, New York (1965)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0037103","volume-title":"Typed Lambda Calculi and Applications","author":"G. Dowek","year":"1993","unstructured":"Dowek, G.: The Undecidability of Typability in the Lambda-Pi-Calculus. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 139\u2013145. Springer, Heidelberg (1993)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0960129598002680","volume":"9","author":"G. Dowek","year":"1999","unstructured":"Dowek, G.: Collections, sets and types. Mathematical Structures in Computer Science\u00a09, 1\u201315 (1999)","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR16","unstructured":"Fitch, F.: Symbolic Logic, An Introduction. The Ronald Press Company (1952)"},{"key":"1_CR17","first-page":"453","volume-title":"H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"R.O. Gandy","year":"1980","unstructured":"Gandy, R.O.: An early proof of normalization by A.M. Turing. In: Seldin, J.P., Hindley, J.R. (eds.) H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 453\u2013455. Academic Press, London (1980)"},{"issue":"4","key":"1_CR18","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1017\/S0960129599002856","volume":"9","author":"H. Geuvers","year":"1999","unstructured":"Geuvers, H., Barendsen, E.: Some logical and syntactical observations concerning the first order dependent type system \u03bbP. Math. Struc. in Comp. Sci.\u00a09(4), 335\u2013360 (1999)","journal-title":"Math. Struc. in Comp. Sci."},{"key":"1_CR19","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and types. Cambridge tracts in theoretical computer science, vol.\u00a07. Cambridge University Press, Cambridge"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"Girard, J.-Y.: The system F of variable types, fifteen years later. Theoretical Computer Science\u00a045, 159\u2013192 (1986)","journal-title":"Theoretical Computer Science"},{"key":"1_CR21","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0049-237X(08)70843-7","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"J.-Y. Girard","year":"1971","unstructured":"Girard, J.-Y.: Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types. In: Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 63\u201392. North-Holland, Amsterdam (1971)"},{"key":"1_CR22","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. In: Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS 1987, Ithaca, NY, USA, June 22-25 (1987)"},{"key":"1_CR23","first-page":"29","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"Hindley, J.R.: The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society\u00a0146, 29\u201360 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"1_CR24","series-title":"London Mathematical Society Student Texts","volume-title":"Introduction to combinators and lambda-calculus","author":"J.R. Hindley","year":"1986","unstructured":"Hindley, J.R., Seldin, J.P.: Introduction to combinators and lambda-calculus. London Mathematical Society Student Texts. Cambridge University Press, Cambridge (1986)"},{"key":"1_CR25","first-page":"479","volume-title":"H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"W. Howard","year":"1980","unstructured":"Howard, W.: The formulas-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479\u2013490. Academic Press, New York (1980)"},{"issue":"1","key":"1_CR26","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","volume":"42","author":"F. Joachimski","year":"2003","unstructured":"Joachimski, F., Matthes, R.: Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and G\u00f6del\u2019s T. Arch. Math. Log.\u00a042(1), 59\u201387 (2003)","journal-title":"Arch. Math. Log."},{"key":"1_CR27","volume-title":"Introduction to Higher Order Categorical Logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)"},{"key":"1_CR28","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory, Bibliopolis (1984)"},{"key":"1_CR29","first-page":"348","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R., Robin: A Theory of Type Polymorphism in Programming. JCSS\u00a017, 348\u2013375 (1978)","journal-title":"JCSS"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-12925-1_41","volume-title":"International Symposium on Programming","author":"A. Mycroft","year":"1984","unstructured":"Mycroft, A.: Polymorphic type schemes and recursive definitions. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol.\u00a0167, pp. 217\u2013228. Springer, Heidelberg (1984)"},{"key":"1_CR31","series-title":"Studies in Logic","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"Nederpelt, R., Geuvers, H., de Vrijer, R. (eds.): Selected Papers on Automath. Studies in Logic, vol.\u00a0133. North-Holland, Amsterdam (1994)"},{"key":"1_CR32","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory, An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory, An Introduction. Oxford University Press, Oxford (1990)"},{"key":"1_CR33","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"2","key":"1_CR34","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G.: Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comp. Sci.\u00a01(2), 125\u2013159 (1975)","journal-title":"Theor. Comp. Sci."},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. Plotkin","year":"1977","unstructured":"Plotkin, G.: LCF considered as a programming language. Theor. Comp. Sci.\u00a05, 223\u2013255 (1977)","journal-title":"Theor. Comp. Sci."},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-13346-1_7","volume-title":"Semantics of Data Types","author":"J.C. Reynolds","year":"1984","unstructured":"Reynolds, J.C.: Polymorphism is not Set-Theoretic. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds.) Semantics of Data Types 1984. LNCS, vol.\u00a0173, pp. 145\u2013156. Springer, Heidelberg (1984)"},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BF02276799","volume":"17","author":"H. Schwichtenberg","year":"1976","unstructured":"Schwichtenberg, H.: Definierbare Funktionen im \u03bb-Kalk\u00fcl mit Typen. Archiv f\u00fcr Mathematische Logik und Grundlagenforschung\u00a017, 113\u2013114 (1976)","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"issue":"2","key":"1_CR38","doi-asserted-by":"publisher","first-page":"187","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretation of functionals of finite type. J. Symbol. Logic\u00a032(2), 187\u2013199 (1967)","journal-title":"J. Symbol. Logic"},{"key":"1_CR39","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"P. Urzyczyn","year":"2006","unstructured":"Urzyczyn, P., S\u00f8rensen, M.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol.\u00a0149. Elsevier, Amsterdam (2006)"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Wand, M.: A simple algorithm and proof for type inference. Fundamenta Informaticae X, 115\u2013122 (1987)","DOI":"10.3233\/FI-1987-10202"},{"key":"1_CR41","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1109\/LICS.1994.316068","volume-title":"Proceedings of the 9th Annual Symposium on Logic in Computer Science","author":"J.B. Wells","year":"1994","unstructured":"Wells, J.B.: Typability and type-checking in the second-order \u03bb-calculus are equivalent and undecidable. In: Proceedings of the 9th Annual Symposium on Logic in Computer Science, Paris, France, pp. 176\u2013185. IEEE Computer Society Press, Los Alamitos (1994)"}],"container-title":["Lecture Notes in Computer Science","Language Engineering and Rigorous Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03153-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T13:34:17Z","timestamp":1710509657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03153-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642031526","9783642031533"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03153-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}