{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:30Z","timestamp":1725664710035},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:35:44Z","timestamp":1330292144000},"page":"291-307","source":"Crossref","is-referenced-by-count":1,"title":["A logical aspect of parametric polymorphism"],"prefix":"10.1007","author":[{"given":"Ryu","family":"Hasegawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","volume":"121","author":"M. Abadi","year":"1993","unstructured":"M. Abadi, L. Cardelli, and P.-L. Curien, Formal parametric polymorphism, Theoret. Comput. Sci. 121 (1993) 9\u201358.","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E. S. Bainbridge","year":"1990","unstructured":"E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott, Functorial polymorphism, Theoret. Comput. Sci. 70 (1990) 35\u201364; Corrigendum, 71 (1990) 431.","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR3","unstructured":"H. P. Barendregt, The lambda calculus, Its syntax and semantics, revised edition, (North-Holland, 1984)."},{"key":"17_CR4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"C. B\u00f6hm and A. Berarducci, Automatic synthesis of typed \u039b-programs on term algebras, Theoret. Comput. Sci. 39 (1985) 135\u2013154.","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0304-3975(93)90057-Z","volume":"115","author":"P. Freyd","year":"1993","unstructured":"P. Freyd, Structural polymorphism, Theoret. Comput. Sci. 115 (1993) 107\u2013129.","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR6","unstructured":"J.-Y. Girard, Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur, Th\u00e8se d'Etat, Universit\u00e9 Paris VII (1972)."},{"key":"17_CR7","unstructured":"J.-Y. Girard, Proof Theory and Logical Complexity, Volume I, Studies in Proof Theory, (Bibliopolis, 1987)."},{"key":"17_CR8","unstructured":"J.-Y. Girard, P. Taylor and Y. Lafont, Proofs and Types, (Cambridge University Press, 1989)."},{"key":"17_CR9","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"K. G\u00f6del, \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes, Dialectica 12 (1958) 280\u2013287; English translation in J. Philosophical Logic 9 (1980) 133\u2013142; reprinted in Kurt G\u00f6del, Collected Works, Volume II, Publications 1938\u20131974, S. Feferman et al., eds., (Oxford University Press, 1990) pp. 240\u2013251.","journal-title":"Dialectica"},{"key":"17_CR10","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1017\/S0960129500000372","volume":"4","author":"R. Hasegawa","year":"1994","unstructured":"R. Hasegawa, Categorical data types in parametric polymorphism, Math. Struct. Comput. Sci. 4 (1994) 71\u2013109.","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR11","first-page":"535","volume":"30","author":"R. Hasegawa","year":"1994","unstructured":"R. Hasegawa, Relational limits in general polymorphism, Publ. Research Institute for Mathematical Sciences 30 (1994) 535\u2013576.","journal-title":"Publ. Research Institute for Mathematical Sciences"},{"key":"17_CR12","unstructured":"J. R. Hindley and J. P. Seldin, Introduction to Combinators and \u03bb-Calculus, (London Math. Soc., 1986)."},{"key":"17_CR13","unstructured":"S. C. Kleene, Introduction to Metamathematics, (North-Holland, 1964)."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"D. Leivant, Reasoning about functional programs and complexity classes associated with type disciplines, in: IEEE 24th Annual Symp. on Foundations of Computer Science, (IEEE, 1983) pp. 460\u2013469.","DOI":"10.1109\/SFCS.1983.50"},{"key":"17_CR15","unstructured":"R. Loader, Models of linear logic and inductive datatypes, Mathematical Institute, Oxford University, preprint (1994)."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"G. Plotkin and M. Abadi, A logic for parametric polymorphism, in: Typed Lambda Calculi and Applications, M. Bezem, J. F. Groote, eds., 1993, Utrecht, The Netherlands, Lecture Notes in Computer Science 664, (Springer, 1993) 361\u2013375.","DOI":"10.1007\/BFb0037118"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds, Towards a theory of type structure, in: B. Robinet ed., Programming Symposium, Paris, Lecture Notes in Computer Science 19 (Springer, 1974) pp. 408\u2013425.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"17_CR18","unstructured":"J. C. Reynolds, Types, abstraction, and parametric polymorphism, in: Information Processing 83, R. E. A. Mason, ed., (North-Holland, 1983) pp. 513\u2013523."},{"key":"17_CR19","doi-asserted-by":"crossref","first-page":"969","DOI":"10.2307\/2273831","volume":"52","author":"R. A. G. Seely","year":"1987","unstructured":"R. A. G. Seely, Categorical semantics for higher order polymorphic lambda calculus, J. Symbolic Logic 52 (1987) 969\u2013989.","journal-title":"J. Symbolic Logic"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"R. M. Smullyan, Theory of Formal Systems, Annals of Mathematics Studies 47, (Princeton University Press, 1961).","DOI":"10.1515\/9781400882007"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"C. Spector, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, in: Recursive Function Theory, J. C. E. Dekker, ed., Proceedings of Symposia in Pure Mathematics, Volume V, (AMS, 1962) pp. 1\u201327.","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"R. Statman, Number theoretic functions computable by polymorphic programs (extended abstract), in: IEEE 22nd Annual Symp. on Foundations of Computer Science, Los Angels, 1981 (IEEE, 1981) pp. 279\u2013282.","DOI":"10.1109\/SFCS.1981.24"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra, Mathematical Investigations of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344, (Springer, 1973).","DOI":"10.1007\/BFb0066739"},{"key":"17_CR24","unstructured":"A. S. Troelstra, Introductory note to 1958 and 1972, in: Kurt G\u00f6del, Collected Works, Volume II, Publications 1938\u20131974, S. Feferman et al., eds., (Oxford University Press, 1990) pp. 217\u2013241."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:05:52Z","timestamp":1605647152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}