{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:56Z","timestamp":1775790836679,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198045","type":"print"},{"value":"9783642198052","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19805-2_8","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T13:05:14Z","timestamp":1300107914000},"page":"108-122","source":"Crossref","is-referenced-by-count":20,"title":["Realizability and Parametricity in Pure Type Systems"],"prefix":"10.1007","author":[{"given":"Jean-Philippe","family":"Bernardy","sequence":"first","affiliation":[]},{"given":"Marc","family":"Lasson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","first-page":"157","volume-title":"Proc. of POPL 1993","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Cardelli, L., Curien, P.: Formal parametric polymorphism. In: Proc. of POPL 1993, pp. 157\u2013170. ACM, New York (1993)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Handbook of Logic in Computer Science, vol.\u00a02, pp. 117\u2013309 (1992)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"8_CR3","unstructured":"Berardi, S.: Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino (1989)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-11957-6_8","volume-title":"Programming Languages and Systems","author":"J.-P. Bernardy","year":"2010","unstructured":"Bernardy, J.-P., Jansson, P., Claessen, K.: Testing polymorphic properties. In: Gordon, A. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 125\u2013144. Springer, Heidelberg (2010)"},{"key":"8_CR5","first-page":"345","volume-title":"Proc. of ICFP 2010","author":"J.-P. Bernardy","year":"2010","unstructured":"Bernardy, J.-P., Jansson, P., Paterson, R.: Parametricity and dependent types. In: Proc. of ICFP 2010, pp. 345\u2013356. ACM, New York (2010)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-24849-1_8","volume-title":"Types for Proofs and Programs","author":"E. Brady","year":"2004","unstructured":"Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 115\u2013129. Springer, Heidelberg (2004)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/165180.165214","volume-title":"Proc. of FPCA","author":"A. Gill","year":"1993","unstructured":"Gill, A., Launchbury, J., Peyton Jones, S.: A short cut to deforestation. In: Proc. of FPCA, pp. 223\u2013232. ACM, New York (1993)"},{"key":"8_CR8","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionnelle et elimination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e9se d\u2019\u00e9tat, Universit\u00e9 de Paris 7 (1972)"},{"issue":"4","key":"8_CR9","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF01360048","volume":"132","author":"R. Harrop","year":"1956","unstructured":"Harrop, R.: On disjunctions and existential statements in intuitionistic systems of logic. Mathematische Annalen\u00a0132(4), 347\u2013361 (1956)","journal-title":"Mathematische Annalen"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S.C. Kleene","year":"1945","unstructured":"Kleene, S.C.: On the interpretation of intuitionistic number theory. J. of Symbolic Logic\u00a010(4), 109\u2013124 (1945)","journal-title":"J. of Symbolic Logic"},{"key":"8_CR11","unstructured":"Kleene, S.C.: Introduction to metamathematics. Wolters-Noordhoff (1971)"},{"key":"8_CR12","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in mathematics, pp. 101\u2013128 (1959)"},{"key":"8_CR13","unstructured":"Krivine, J.-L.: Lambda-calcul types et mod\u00e8les. Masson (1990)"},{"issue":"3","key":"8_CR14","first-page":"149","volume":"26","author":"J.-L. Krivine","year":"1990","unstructured":"Krivine, J.-L., Parigot, M.: Programming with proofs. J. Inf. Process. Cybern.\u00a026(3), 149\u2013167 (1990)","journal-title":"J. Inf. Process. Cybern."},{"key":"8_CR15","unstructured":"Leivant, D.: Contracting proofs to programs. Logic and Comp. Sci., pp. 279\u2013327 (1990)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3540543961_15","volume-title":"Functional Programming Languages and Computer Architecture","author":"H. Mairson","year":"1991","unstructured":"Mairson, H.: Outline of a proof theory of parametricity. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol.\u00a0523, pp. 313\u2013327. Springer, Heidelberg (1991)"},{"issue":"01","key":"8_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program.\u00a014(01), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Milner, R.: Logic for Computable Functions: description of a machine implementation. Artificial Intelligence (1972)","DOI":"10.21236\/AD0785072"},{"key":"8_CR19","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers Tekniska H\u00f6gskola (2007)"},{"key":"8_CR20","first-page":"89","volume-title":"POPL 1989","author":"C. Paulin-Mohring","year":"1989","unstructured":"Paulin-Mohring, C.: Extracting F\u03c9\u2019s programs from proofs in the calculus of constructions. In: POPL 1989, pp. 89\u2013104. ACM, New York (1989)"},{"key":"8_CR21","unstructured":"Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris 7 (1989)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G. Plotkin","year":"1993","unstructured":"Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 361\u2013375. Springer, Heidelberg (1993)"},{"issue":"1","key":"8_CR23","first-page":"513","volume":"83","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. Information processing\u00a083(1), 513\u2013523 (1983)","journal-title":"Information processing"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0066777","volume-title":"Cambridge Summer School in Mathematical Logic","author":"John Staples","year":"1973","unstructured":"Staples, J.: Combinator realizability of constructive finite type analysis. Cambridge Summer School in Mathematical Logic, pp. 253\u2013273 (1973)"},{"key":"8_CR25","unstructured":"The Coq development team. The Coq proof assistant (2010)"},{"key":"8_CR26","volume-title":"Handbook of proof theory","author":"A. Troelstra","year":"1998","unstructured":"Troelstra, A.: Realizability. In: Handbook of proof theory. Elsevier, Amsterdam (1998)"},{"issue":"03","key":"8_CR27","first-page":"239","volume":"12","author":"J. Oosten Van","year":"2002","unstructured":"Van Oosten, J.: Realizability: a historical essay. Mathematical Structures in Comp. Sci.\u00a012(03), 239\u2013263 (2002)","journal-title":"Mathematical Structures in Comp. Sci."},{"key":"8_CR28","first-page":"347","volume-title":"Proc. of FPCA 1989","author":"P. Wadler","year":"1989","unstructured":"Wadler, P.: Theorems for free. In: Proc. of FPCA 1989, pp. 347\u2013359. ACM, New York (1989)"},{"issue":"1\u20133","key":"8_CR29","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/j.tcs.2006.12.042","volume":"375","author":"P. Wadler","year":"2007","unstructured":"Wadler, P.: The Girard\u2013Reynolds isomorphism. Theor. Comp. Sci.\u00a0375(1\u20133), 201\u2013226 (2007)","journal-title":"Theor. Comp. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T04:43:03Z","timestamp":1712292183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}