{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:27Z","timestamp":1725663567257},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540543961"},{"type":"electronic","value":"9783540475996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3540543961_15","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:43:13Z","timestamp":1330209793000},"page":"313-327","source":"Crossref","is-referenced-by-count":13,"title":["Outline of a proof theory of parametricity"],"prefix":"10.1007","author":[{"given":"Harry G.","family":"Mairson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,7,6]]},"reference":[{"key":"15_CR1","unstructured":"R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall, 1988."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"C. B\u00f6hm and A. Berarducci. Automatic synthesis of typed \u03bb-programs on term algebras. Theoretical Computer Science 39, pp. 135\u2013154.","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"K. Bruce, J. C. Mitchell, and A. R. Meyer. The semantics of second-order lambda-calculus. In Logical Foundations of Functional Programming, ed. G. Huet, pp. 213\u2013272. Addison Wesley, 1990.","DOI":"10.1016\/0890-5401(90)90044-I"},{"key":"15_CR4","unstructured":"D. van Daalen. Logic and Structure. Springer-Verlag, 1979."},{"key":"15_CR5","unstructured":"J.-Y. Girard, Interpr\u00e9tation Fonctionelle et Elimination des Coupures de l'Arithmetique d'Ordre Superieur. Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Paris VII, 1972."},{"key":"15_CR6","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989."},{"key":"15_CR7","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 nict ben\u00fcte Erweiterung des finiten Standpunktes. Dialectica 12 (1958), pp. 280\u2013287. Republished with English translation and explanatory notes by A. S. Troelstra in Kurt G\u00f6del: Collected Works (Oxford University Press, 1990), vol. II, ed. S. Feferman.","journal-title":"Dialectica"},{"key":"15_CR8","unstructured":"W. Howard. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, ed. J. Seldin and R. Hindley, pp. 479\u2013490. Academic Press, 1980."},{"key":"15_CR9","unstructured":"D. Leivant. Contracting proofs to programs. In Logic and Computer Science, ed. P. Odifreddi, pp. 279\u2013328. Academic Press, 1990."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"F. Henglein and H. Mairson. The complexity of type inference for higher-order typed lambda calculi. Proceedings of the 18-th ACM Symposium on the Principles of Programming Languages, January 1991, pp. 119\u2013130.","DOI":"10.1145\/99583.99602"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell. Type systems for programming languages. Handbook of Theoretical Computer Science, van Leeuwen et al., eds. North-Holland, 1990, pp. 365\u2013458.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"15_CR12","unstructured":"B. Pierce, S. Dietzen, and S. Michaylov. Programming in higher-order typed lambda calculi. Technical Report CMU-CS-89-111, Carnegie Mellon University, March 1989."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Towards a theory of type structure. In Proceedings of the Paris Colloquium on Programming, Lecture Notes in Computer Science 19, Springer Verlag, pages 408\u2013425, 1974.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"15_CR14","unstructured":"J. C. Reynolds. Introduction to polymorphic lambda-calculus. In Logical Foundations of Functional Programming, ed. G. Huet, pp. 77\u201386. Addison Wesley, 1990."},{"key":"15_CR15","unstructured":"J. C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing 83, ed. R. E. A. Mason, pp. 513\u2013523. Elsevier, 1983."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"A. Scedrov. A guide to polymorphic types. In Logic and Computer Science, ed. P. Odifreddi, pp. 387\u2013420. Academic Press, 1990.","DOI":"10.1007\/BFb0093926"},{"key":"15_CR17","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman. Logical relations and the typed lambda calculus. Information and Control 65 (1985), pp. 85\u201397.","journal-title":"Information and Control"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"P. Wadler. Theorems for free! In 4th International Symposium on Functional Programming Languages and Computer Architecture, London, September 1989.","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Functional Programming Languages and Computer Architecture"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3540543961_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:54Z","timestamp":1605646434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3540543961_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540543961","9783540475996"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3540543961_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}