{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:48Z","timestamp":1779836748774,"version":"3.53.1"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2011,9,7]],"date-time":"2011-09-07T00:00:00Z","timestamp":1315353600000},"content-version":"unspecified","delay-in-days":6,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2011,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Type abstraction and intensional type analysis are features seemingly at odds\u2014type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implemented \u201cdynamic type generation\u201d as a way to reconcile these features. The idea is that, when one defines an abstract type, one should also be able to generate at runtime a fresh type name, which may be used as a dynamic representative of the abstract type for purposes of type analysis. The question remains: in a language with non-parametric polymorphism, does dynamic type generation provide us with the same kinds of abstraction guarantees that we get from parametric polymorphism?<\/jats:p>\n                  <jats:p>Our goal is to provide a rigorous answer to this question. We define a step-indexed Kripke logical relation for a language with both non-parametric polymorphism (in the form of type-safe cast) and dynamic type generation. Our logical relation enables us to establish parametricity and representation independence results, even in a non-parametric setting, by attaching arbitrary relational interpretations to dynamically generated type names. In addition, we explore how programs that are provably equivalent in a more traditional parametric logical relation may be \u201cwrapped\u201d systematically to produce terms that are related by our non-parametric relation, and vice versa. This leads us to develop a \u201cpolarized\u201d variant of our logical relation, which enables us to distinguish formally between positive and negative notions of parametricity.<\/jats:p>","DOI":"10.1017\/s0956796811000165","type":"journal-article","created":{"date-parts":[[2011,9,7]],"date-time":"2011-09-07T11:10:20Z","timestamp":1315393820000},"page":"497-562","source":"Crossref","is-referenced-by-count":13,"title":["Non-parametric parametricity"],"prefix":"10.1017","volume":"21","author":[{"given":"GEORG","family":"NEIS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DEREK","family":"DREYER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREAS","family":"ROSSBERG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2011,9,7]]},"reference":[{"key":"S0956796811000165_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"S0956796811000165_ref18","first-page":"122","volume-title":"Proceedings of International Symposium on Mathematical Foundations of Computer Science (MFCS)","author":"Pitts","year":"1993"},{"key":"S0956796811000165_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(99)00036-8"},{"key":"S0956796811000165_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"S0956796811000165_ref16","doi-asserted-by":"crossref","unstructured":"Neis G. (2009) Non-Parametric Parametricity. M.Phil. thesis, Universit\u00e4t des Saarlandes.","DOI":"10.1145\/1596550.1596572"},{"key":"S0956796811000165_ref27","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11403"},{"key":"S0956796811000165_ref17","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts","year":"2005"},{"key":"S0956796811000165_ref25","doi-asserted-by":"crossref","unstructured":"Sewell P. (2001) Modules, abstract types, and distributed versioning. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 236\u2013247.","DOI":"10.1145\/360204.360225"},{"key":"S0956796811000165_ref9","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation Fonctionelle et \u00c9limination des Coupures de L'arithm\u00e9tique D'ordre Sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0956796811000165_ref8","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2828"},{"key":"S0956796811000165_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006442"},{"key":"S0956796811000165_ref24","unstructured":"Rossberg A. , Le Botlan D. , Tack G. , Brunklaus T. & Smolka G. (2004) Alice ML through the looking glass. In Proceedings of Symposium on Trends in Functional Programming (TFP), vol. 5, pp. 79\u201396."},{"key":"S0956796811000165_ref22","unstructured":"Rossberg A. (2007) Typed Open Programming: A Higher-Order, Typed Approach to Dynamic Modularity and Distribution. Ph.D. thesis, Universit\u00e4t des Saarlandes."},{"key":"S0956796811000165_ref7","doi-asserted-by":"crossref","unstructured":"Benton N. & Tabareau N. (2009) Compiling functional types to relational specifications for low level imperative code. In Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), pp. 3\u201314.","DOI":"10.1145\/1481861.1481864"},{"key":"S0956796811000165_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"S0956796811000165_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888274"},{"key":"S0956796811000165_ref19","unstructured":"Pitts A. & Stark I. (1998) Operational reasoning for functions with local state. In Proceedings of Higher Order Operational Techniques in Semantics (HOOTS), pp. 227\u2013274."},{"key":"S0956796811000165_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005179"},{"key":"S0956796811000165_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"S0956796811000165_ref2","unstructured":"Ahmed A. (2004) Semantics of Types for Mutable State. Ph.D. thesis, Princeton University."},{"key":"S0956796811000165_ref14","doi-asserted-by":"crossref","unstructured":"Mitchell J. C. (1986) Representation independence and data abstraction. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 263\u2013276.","DOI":"10.1145\/512644.512669"},{"key":"S0956796811000165_ref20","first-page":"513","volume-title":"Inf. Process","author":"Reynolds","year":"1983"},{"key":"S0956796811000165_ref13","unstructured":"Matthews J. & Ahmed A. (2008) Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In Proceedings of European Symposium on Programming (ESOP), pp. 16\u201331."},{"key":"S0956796811000165_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/371880.371887"},{"key":"S0956796811000165_ref31","unstructured":"Wadler P. (1989) Theorems for free! In Proceedings of Conference on Functional Programming and Computer Architecture, pp. 347\u2013359."},{"key":"S0956796811000165_ref30","doi-asserted-by":"crossref","unstructured":"Vytiniotis D. , Washburn G. & Weirich S. (2005) An open and shut typecase. In Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), pp. 13\u201324.","DOI":"10.1145\/1040294.1040296"},{"key":"S0956796811000165_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.019"},{"key":"S0956796811000165_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"S0956796811000165_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0956796811000165_ref12","unstructured":"Harper R. & Morrisett G. (1995) Compiling polymorphism using intensional type analysis. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 130\u2013141."},{"key":"S0956796811000165_ref32","unstructured":"Washburn G. & Weirich S. (2005) Generalizing parametricity using information flow. In Proceedings of Symposium on Logic in Computer Science, pp. 62\u201371."},{"key":"S0956796811000165_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480925"},{"key":"S0956796811000165_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.032"},{"key":"S0956796811000165_ref4","doi-asserted-by":"crossref","unstructured":"Ahmed A. & Blume M. (2008) Typed closure conversion preserves observational equivalence. In Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 157\u2013168.","DOI":"10.1145\/1411204.1411227"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796811000165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:24Z","timestamp":1779834984000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796811000165\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9]]},"references-count":34,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["S0956796811000165"],"URL":"https:\/\/doi.org\/10.1017\/s0956796811000165","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9]]}}}