Abstract
We show that there exist bijective translations between polymorphic λ-calculus and a subsystem of minimal logic with existential types, which form a Galois connection and moreover a Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.
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
Coquand, T.: An analysis of Girard’s paradox. In: Proc. the Annual IEEE Symposium on Logic in Computer Science, pp. 227–236 (1986)
Fujita, K.: A sound and complete CSP-translation for λμ-Calculus. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 120–134. Springer, Heidelberg (2003)
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)
Hofmann, M., Streicher, T.: Continuation models are universal for λμ-calculus. In: Proc. the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 387–395 (1997)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. In: Proc. the 12th Annual ACM Symposium on Principles of Programming Languages, pp. 37–51 (1985)
Parigot, M.: λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Plotkin, G.: Call-by-Name, Call-by-Value and the λ-Calculus. Theoretical Computer Science 1, 125–159 (1975)
Prawitz, D.: Natural Deduction, A Proof Theoretical Study. Almqvist & Wiksell, Stockholm (1965)
Selinger, P.: Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Math. Struct. in Compu. Science 11, 207–260 (2001)
Sabry, A., Felleisen, M.: Reasoning about Programs in Continuation-Passing Style. Lisp and Symbolic Computation: An International Journal 6, 289–360 (1993)
Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems 19-6, 916–941 (1997)
Thielecke, H.: Answer type polymorphism in call-by-name continuation passing. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 279–293. Springer, Heidelberg (2004)
Wadler, P.: Call-by-value is dual to call-by-name. In: International Conference on Functional Programming, Uppsala, August 25-29 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fujita, Ke. (2005). Galois Embedding from Polymorphic Types into Existential Types. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_15
Download citation
DOI: https://doi.org/10.1007/11417170_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)