{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:35Z","timestamp":1767929315655,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642171635","type":"print"},{"value":"9783642171642","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_24","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T10:54:39Z","timestamp":1290164079000},"page":"344-359","source":"Crossref","is-referenced-by-count":10,"title":["Relational Parametricity for a Polymorphic Linear Lambda Calculus"],"prefix":"10.1007","author":[{"given":"Jianzhou","family":"Zhao","sequence":"first","affiliation":[]},{"given":"Qi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A. Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"issue":"1","key":"24_CR2","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1145\/1594834.1480925","volume":"44","author":"A. Ahmed","year":"2009","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. SIGPLAN Not.\u00a044(1), 340\u2013353 (2009)","journal-title":"SIGPLAN Not."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"24_CR4","unstructured":"Barber, A.: Linear Type Theories, Semantics and Action Calculi. PhD thesis, Edinburgh University (1997)"},{"issue":"2","key":"24_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S0956796899003639","volume":"10","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M.: Program equivalence in a linear functional language. J. Funct. Program.\u00a010(2), 167\u2013190 (2000)","journal-title":"J. Funct. Program."},{"key":"24_CR6","series-title":"ENTCS","volume-title":"Proc. of HOOTS","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M., Pitts, A.M., Russo, C.V.: Operational properties of lily, a polymorphic linear lambda calculus with recursion. In: Proc. of HOOTS. ENTCS, vol.\u00a041. Elsevier, Amsterdam (2000)"},{"issue":"5:1","key":"24_CR7","first-page":"1","volume":"2","author":"L. Birkedal","year":"2006","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Petersen, R.L.: Linear Abadi and Plotkin logic. Logical Methods in Computer Science\u00a02(5:1), 1\u201333 (2006)","journal-title":"Logical Methods in Computer Science"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1481861.1481873","volume-title":"TLDI 2009: Proceedings of the 4th International Workshop on Types in Language Design and Implementation","author":"L. Birkedal","year":"2009","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: TLDI 2009: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, pp. 91\u2013104. ACM, New York (2009)"},{"key":"24_CR9","unstructured":"The Coq Development\u00a0Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009), http:\/\/coq.inria.fr"},{"key":"24_CR10","volume-title":"Advanced Topics in Types and Programming Languages","author":"K. Crary","year":"2005","unstructured":"Crary, K.: Logical Relations and a Case Study in Equivalence Checking. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)"},{"issue":"1","key":"24_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1093\/jigpal\/9.1.27","volume":"9","author":"R.L. Crole","year":"2001","unstructured":"Crole, R.L.: Completeness of bisimilarity for contextual equivalence in linear theories. Logic Jnl IGPL\u00a09(1), 27\u201351 (2001)","journal-title":"Logic Jnl IGPL"},{"issue":"5","key":"24_CR12","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.entcs.2007.01.021","volume":"174","author":"K. Donnelly","year":"2007","unstructured":"Donnelly, K., Xi, H.: A formalization of strong normalization for simply-typed lambda-calculus and System F. Electron. Notes Theor. Comput. Sci.\u00a0174(5), 109\u2013125 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"#cr-split#-24_CR13.1","unstructured":"Girard, J.-Y.: Interpr??tation fonctionnelle et ??limination des coupures de l???arith m?? tique d???ordre sup??rieur. Th??se d?????tat (1972);"},{"key":"#cr-split#-24_CR13.2","unstructured":"Summary in Fenstad, J.E. (ed.): Scandinavian Logic Symposium, pp. 63???92. North-Holland, Amsterdam (1971)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-48959-2_15","volume-title":"Typed Lambda Calculi and Applications","author":"M. Hasegawa","year":"1999","unstructured":"Hasegawa, M.: Logical predicates for intuitionistic linear type theories. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 198\u2013213. Springer, Heidelberg (1999)"},{"issue":"3","key":"24_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I. Mason","year":"1991","unstructured":"Mason, I., Talcott, C.: Equivalence in functional languages with effects. J. Funct. Program.\u00a01(3), 245\u2013285 (1991)","journal-title":"J. Funct. Program."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Mazurak, K., Zhao, J., Zdancewic, S.: Lightweight linear types in system $\\textrm{F}^{\\o}$ . In: TLDI 2010: Proceedings of the 4th International Workshop on Types in Language Design and Implementation (2010)","DOI":"10.1145\/1708016.1708027"},{"key":"24_CR17","volume-title":"Advanced Topics in Types and Programming Languages","author":"A. Pitts","year":"2005","unstructured":"Pitts, A.: Typed Operational Reasoning. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)"},{"key":"24_CR18","first-page":"513","volume-title":"Information Processing","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C.: Types, abstraction, and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing, pp. 513\u2013523. Elsevier Science Publishers B.V., Amsterdam (1983)"},{"key":"24_CR19","unstructured":"Sch\u00fcrmann, C., Sarnat, J.: Towards a judgmental reconstruction of logical relation proofs. Technical report, Yale University (2006)"},{"issue":"1","key":"24_CR20","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strni\u0161a, R.: Ott: Effective Tool Support for the Working Semanticist. J. Funct. Program.\u00a020(1), 71\u2013122 (2010)","journal-title":"J. Funct. Program."},{"issue":"2","key":"24_CR21","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic\u00a032(2), 198\u2013212 (1967)","journal-title":"Journal of Symbolic Logic"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1016\/j.entcs.2007.02.043","volume":"173","author":"D. Vytiniotis","year":"2007","unstructured":"Vytiniotis, D., Weirich, S.: Free theorems and runtime type representations. Electron. Notes Theor. Comput. Sci.\u00a0173, 357\u2013373 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the 4th International Symposium on Functional Programming and Computer Architecture (September 1989)","DOI":"10.1145\/99370.99404"},{"key":"24_CR24","volume-title":"Advanced Topics in Types and Programming Languages","author":"D. Walker","year":"2005","unstructured":"Walker, D.: Substructural Type Systems. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Zhao, J., Zhang, Q., Zdancewic, S.: Relational parametricity for a polymorphic linear lambda calculus. Technical report (2010), http:\/\/www.cis.upenn.edu\/~jianzhou\/parametricity4linf","DOI":"10.1007\/978-3-642-17164-2_24"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T07:16:32Z","timestamp":1685862992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}