Abstract
This paper presents a novel syntactic logical relation for a polymorphic linear λ-calculus that treats all types as linear and introduces the constructor ! to account for intuitionistic terms, and System F°—an extension of System F that uses kinds to distinguish linear from intuitionistic types. We define a logical relation for open values under both open linear and intuitionistic contexts, then extend it for open terms with evaluation and open relation substitutions. Relations that instantiate type quantifiers are for open terms and types. We demonstrate the applicability of this logical relation through its soundness with respect to contextual equivalence, along with free theorems for linearity that are difficult to achieve by closed logical relations. When interpreting types on only closed terms, the model defaults to a closed logical relation that is both sound and complete with respect to contextual equivalence and is sufficient to reason about isomorphisms of type encodings. All of our results have been mechanically verified in Coq.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69–83. Springer, Heidelberg (2006)
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. SIGPLAN Not. 44(1), 340–353 (2009)
Aydemir, B., Charguéraud, 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)
Barber, A.: Linear Type Theories, Semantics and Action Calculi. PhD thesis, Edinburgh University (1997)
Bierman, G.M.: Program equivalence in a linear functional language. J. Funct. Program. 10(2), 167–190 (2000)
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. 41. Elsevier, Amsterdam (2000)
Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Linear Abadi and Plotkin logic. Logical Methods in Computer Science 2(5:1), 1–33 (2006)
Birkedal, L., Støvring, 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–104. ACM, New York (2009)
The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009), http://coq.inria.fr
Crary, K.: Logical Relations and a Case Study in Equivalence Checking. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)
Crole, R.L.: Completeness of bisimilarity for contextual equivalence in linear theories. Logic Jnl IGPL 9(1), 27–51 (2001)
Donnelly, K., Xi, H.: A formalization of strong normalization for simply-typed lambda-calculus and System F. Electron. Notes Theor. Comput. Sci. 174(5), 109–125 (2007)
Girard, J.-Y.: Interprétation fonctionnelle et élimination des coupures de l’arith mé tique d’ordre supérieur. Thèse d’état (1972); Summary in Fenstad, J.E. (ed.): Scandinavian Logic Symposium, pp. 63–92. North-Holland, Amsterdam (1971)
Hasegawa, M.: Logical predicates for intuitionistic linear type theories. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 198–213. Springer, Heidelberg (1999)
Mason, I., Talcott, C.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 245–285 (1991)
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)
Pitts, A.: Typed Operational Reasoning. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)
Reynolds, J.C.: Types, abstraction, and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing, pp. 513–523. Elsevier Science Publishers B.V., Amsterdam (1983)
Schürmann, C., Sarnat, J.: Towards a judgmental reconstruction of logical relation proofs. Technical report, Yale University (2006)
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: Ott: Effective Tool Support for the Working Semanticist. J. Funct. Program. 20(1), 71–122 (2010)
Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32(2), 198–212 (1967)
Vytiniotis, D., Weirich, S.: Free theorems and runtime type representations. Electron. Notes Theor. Comput. Sci. 173, 357–373 (2007)
Wadler, P.: Theorems for free! In: Proceedings of the 4th International Symposium on Functional Programming and Computer Architecture (September 1989)
Walker, D.: Substructural Type Systems. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)
Zhao, J., Zhang, Q., Zdancewic, S.: Relational parametricity for a polymorphic linear lambda calculus. Technical report (2010), http://www.cis.upenn.edu/~jianzhou/parametricity4linf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, J., Zhang, Q., Zdancewic, S. (2010). Relational Parametricity for a Polymorphic Linear Lambda Calculus. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)