{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:18Z","timestamp":1761611298514,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525929"},{"type":"electronic","value":"9783540470458"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52592-0_53","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:38:38Z","timestamp":1330205918000},"page":"1-35","source":"Crossref","is-referenced-by-count":18,"title":["Types in lambda calculi and programming languages"],"prefix":"10.1007","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]},{"given":"Kees","family":"Hemerik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"unstructured":"Bakel, S. van. [1990] Complete restrictions of the intersection type discipline. To appear in Theoretical Computer Science.","key":"1_CR1"},{"key":"1_CR2","volume-title":"The lambda calculus, its syntax and semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P. [1984] The lambda calculus, its syntax and semantics, 2-nd revised edition, North Holland Publishing Company, Amsterdam, 1984.","edition":"2-nd revised ed"},{"key":"1_CR3","first-page":"1","volume-title":"Introduction to generalised type systems","author":"H.P. Barendregt","year":"1989","unstructured":"[1989] Introduction to generalised type systems, Proceedings 3rd Italian Conference on Theoretical Computer Science, (Eds. A. Bertoni e.a.), World Scientific, Singapore, 1\u201337."},{"key":"1_CR4","volume-title":"Handbook of Theoretical Computer Science","author":"H.P. Barendregt","year":"1990","unstructured":"[1990] Functional programming and Lambda Calculus. To appear in Handbook of Theoretical Computer Science, (Ed. J. van Leeuwen), North Holland, Amsterdam."},{"key":"1_CR5","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"199-","unstructured":"[199-] Lambda calculi with types. To appear in: Handbook of Logic in Computer Science, (Eds. S. Abramsky, D. Gabbai and T. Maibaum), Oxford University Press, Oxford."},{"issue":"4","key":"1_CR6","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M. [1983] A filter lambda model and the completeness of type assignment, Journal of Symbolic Logic, 48, 4, 931\u2013940.","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR7","first-page":"122","volume-title":"Lecture Notes in Computer Science 224","author":"H.P. Barendregt","year":"1985","unstructured":"Barendregt, H.P. and M. van Leeuwen [1985] Functional programming and the language TALE, in: Lecture Notes in Computer Science 224, Springer, Berlin, 122\u2013208."},{"unstructured":"Barendregt, H.P., Dekkers, W. [199-] Typed lambda calculi, syntax and semantics, to appear.","key":"1_CR8"},{"doi-asserted-by":"crossref","unstructured":"Boehm, H.J. [1989] Type inference in the Presence of Type abstraction, in: SIGPLAN 89 Conference on Programming Languages Design and Implementation, Portland, Oregon 1989.","key":"1_CR9","DOI":"10.1145\/73141.74835"},{"unstructured":"Burstall, R., MacQueen, D., Sanella, D. [1980] HOPE: An experimental applicative language, report CSR-62-80, Edinburgh University.","key":"1_CR10"},{"issue":"4","key":"1_CR11","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli, L., Wegner, P. [1985] On understanding types, data abstraction, and polymorphism, Computing Surveys 17, 4, 471\u2013522.","journal-title":"Computing Surveys"},{"unstructured":"Cardone, F., Coppo, M. [1990] Type inference with recursive types: Syntax and semantics. To appear in Information and Computation.","key":"1_CR12"},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1941","unstructured":"Church, A. [1941] A formalisation of the simple theory of types, Journal of Symbolic Logic 5, 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"unstructured":"[1941a] The calculi of lambda conversion, Princeton University Press; Reprinted 1963 by University Microfilms Inc., Ann Arbor, Michigan, USA.","key":"1_CR14"},{"key":"1_CR15","volume-title":"Implementing mathematics with the nuprl proof development system","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L. et al. [1986] Implementing mathematics with the nuprl proof development system, Prentice-Hall Inc., Englewood Cliffs, New Jersey."},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and G. Huet [1988] The calculus of constructions, Information and Computation 76, 95\u2013120.","journal-title":"Information and Computation"},{"key":"1_CR17","volume-title":"The calculus of constructions, documentation and usersguide, version 4.10","author":"T. Coquand","year":"1989","unstructured":"Coquand, T. et al. [1989] The calculus of constructions, documentation and usersguide, version 4.10, INRIA, Rocquencourt, France."},{"key":"1_CR18","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"H.B. Curry","year":"1934","unstructured":"Curry, H.B. [1934] Functionality in combinatory logic, Proc. Nat. Acad. Science USA 20, 584\u2013590.","journal-title":"Proc. Nat. Acad. Science USA"},{"doi-asserted-by":"crossref","unstructured":"Damas, L. [1982] Principal type schemes for functional programming, Proceedings of the 9th ACM-POPL, 207\u2013212.","key":"1_CR19","DOI":"10.1145\/582153.582176"},{"unstructured":"Girard, J.-Y. [1972] Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre superieur. Ph.D. Thesis, Universit\u00e9 Paris VII.","key":"1_CR20"},{"doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C. [1979] A mechanical logic of computation. Edinburgh LCF, Lecture Notes in Computer Science 78, Springer.","key":"1_CR21","DOI":"10.1007\/3-540-09724-4"},{"unstructured":"Harper, R., MacQueen, D., Milner, R. [1986] Standard ML, Report ECS-LFCS-86-2, Edinburgh University.","key":"1_CR22"},{"unstructured":"Harper, R., F. Honsell and G. Plotkin, [1987] A framework for defining logics, Proceedings second Symp. Logic in Computer Science (Ithaca, N. Y.), IEEE, Washington DC, 194\u2013204.","key":"1_CR23"},{"key":"1_CR24","first-page":"29","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"Hindley, J.R. [1969] The principal type-scheme of an object in combinatory logic, Trans. Am. Math. Soc. 146, 29\u201360.","journal-title":"Trans. Am. Math. Soc."},{"unstructured":"Kfoury, A.J., Tiuryn, J., Uryczyn, P. [1988] A proper extension of ML with an effective type assigment, Proceedings of the 15th ACM, POPL.","key":"1_CR25"},{"doi-asserted-by":"crossref","unstructured":"Kfoury, A.J., Tiuryn, J., Uryczyn, P. [1989] Computational consequences and partial solutions of a generalized unification problem. Proceedings of the 4th IEEE-LICS, 98\u2013105.","key":"1_CR26","DOI":"10.1109\/LICS.1989.39163"},{"unstructured":"Lehmann, D.J. [1977] Modes in ALGOL Y. Proceedings 5th Annual I.I.I. conference, may 1977, Guidel, France, Published by INRIA, 1977.","key":"1_CR27"},{"doi-asserted-by":"crossref","unstructured":"McCracken, N.D. [1984] The typechecking of programs with implicit type structure, Semantics of data types, (Eds. G. Kahn e.a.), Lecture Notes in Computer Science 173, Springer, 301\u2013315.","key":"1_CR28","DOI":"10.1007\/3-540-13346-1_15"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0019-9958(86)80019-5","volume":"71","author":"D. MacQueen","year":"1986","unstructured":"MacQueen, D., Plotkin, G., Sethi, R. [1986] An ideal model for recursive polymorphic types, Information and control 71, 95\u2013130.","journal-title":"Information and control"},{"unstructured":"Mendler, N.P. [1987] Inductive types and type constraints in second-order lambda calculus, Proceedings of the 2nd symposium of LICS.","key":"1_CR30"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R. [1978] A theory of type polymorphism in programming, Journal of Comp. Syst. Sci., 17, 348\u2013375.","journal-title":"Journal of Comp. Syst. Sci."},{"key":"1_CR32","volume-title":"Lambda calculus models of programming languages, MAC-TR-57","author":"J.H. Morris","year":"1968","unstructured":"Morris, J.H. [1968] Lambda calculus models of programming languages, MAC-TR-57, Project MAC, MIT, Cambridge, Massachussets."},{"unstructured":"Mycroft, A. [1984] Polymorphic type schemes for functional programs, Proceedings of the 9th ACM POPL.","key":"1_CR33"},{"doi-asserted-by":"crossref","unstructured":"O'Toole, J.W., Gifford, D.K. [1989] Type reconstruction with first-class polymorphic values SIGPLAN 89 Conference on Programming Languages Design and Implementation, Portland, Oregon 1989.","key":"1_CR34","DOI":"10.1145\/73141.74836"},{"doi-asserted-by":"crossref","unstructured":"Pfenning, F. [1988] Partial polymorphic type inference and higher-order unification, Proceedings of the ACM LISP and Functional Programming Conference.","key":"1_CR35","DOI":"10.1145\/62678.62697"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C. [1974] Towards a theory of type structure, in: Proc. of the Colloque sur la Programmation, Paris, Lecture Notes in Computer Science 19, Springer, 408\u2013425.","key":"1_CR36","DOI":"10.1007\/3-540-06859-7_148"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-15198-2_7","volume-title":"Mathematical Foundations of Software Development","author":"J.C. Reynolds","year":"1985","unstructured":"[1985] Three approaches to type structure, in: Mathematical Foundations of Software Development (Eds. Ehring e.a.), Lecture Notes in Computer Science 185, Springer, Berlin, 97\u2013138."},{"unstructured":"[1989] Synctactic control of interference, part 2.","key":"1_CR38"},{"key":"1_CR39","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0167-6423(89)90016-6","volume":"13","author":"R.D. Tennent","year":"1989","unstructured":"Tennent, R.D. [1989] Elementary data structures in ALGOL-like languages. Science of Computer Programming 13 (1989\/90), 73\u2013110.","journal-title":"Science of Computer Programming"},{"key":"1_CR40","series-title":"Nancy, Lecture Notes in Computer Science","first-page":"1","volume-title":"Functional programming languages and computer architecture","author":"D. Turner","year":"1985","unstructured":"Turner, D. [1985] Miranda, a non-strict functional language with polymorphic types, in: Functional programming languages and computer architecture, Nancy, Lecture Notes in Computer Science 201, Springer, Berlin, 1\u201316."},{"doi-asserted-by":"crossref","unstructured":"Wand, M. [1987] A simple algorithm and proof for type inference, Fundamenta Informaticae X, 115\u2013122.","key":"1_CR41","DOI":"10.3233\/FI-1987-10202"},{"key":"1_CR42","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF02163002","volume":"14","author":"A. Wijngaarden van","year":"1969","unstructured":"Wijngaarden, van, A. Mailloux, B, Peck, J.E.L., Koster, C.H.A. [1969] Report on the algorithmic language ALGOL 68, Num. Math. 14, 79\u2013218.","journal-title":"Num. Math."}],"container-title":["Lecture Notes in Computer Science","ESOP '90"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52592-0_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:03:22Z","timestamp":1742591002000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52592-0_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525929","9783540470458"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-52592-0_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}