zbMATH — the first resource for mathematics

CPS-translation as adjoint. (English) Zbl 1186.68101
Summary: We show that there exist translations between polymorphic \(\lambda \)-calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic \(\lambda \)-calculus into the existential type system is the so-called call-by-name CPS-translation that can be expounded as an adjoint from the neat connection. The construction of an inverse translation is investigated from a viewpoint of residuated mappings. The duality appears not only in the reduction relations but also in the proof structures, such as paths between the source and the target calculi. From a programming point of view, this result means that abstract data types can interpret polymorphic functions under the CPS-translation. We may regard abstract data types as a dual notion of polymorphic functions.

68N18 Functional programming and lambda calculus
Full Text: DOI
[1] Backhouse, R., Galois connections and fixed point calculus, (), 89-150 · Zbl 1065.68030
[2] Barendregt, H.P., The lambda calculus, its syntax and semantics, (1984), North-Holland · Zbl 0551.03007
[3] Blyth, T.S., Lattices and ordered algebraic structures, (2005), Springer · Zbl 1073.06001
[4] Curien, P.-L.; Hardin, Th., A simple proof of non confluence of lambda-calculus with surjective pairing, The types forum, 7, (1991)
[5] O. Danvy, J.L. Lawall, Back to direct style II: First-class continuations, in: Proc. of the ACM Conference on Lisp and Functional Programming, 1992, pp. 299-310
[6] Filinski, A., Declarative continuations: an investigation of duality in programming language semantics, (), 224-249
[7] Fujita, K., Domain-free \(\lambda \mu\)-calculus, Theoretical informatics and applications, 34, 433-466, (2000) · Zbl 0974.68032
[8] Fujita, K., Simple models of type free \(\lambda \mu\)-calculus, Computer software, 20, 3, 73-79, (2003)
[9] Fujita, K., A sound and complete CSP-translation for \(\lambda \mu\)-calculus, (), 120-134 · Zbl 1040.03008
[10] Fujita, K., Galois embedding from polymorphic types into existential types, (), 194-208 · Zbl 1114.03009
[11] Hasegawa, M., Relational parametricity and control (extended abstract), Proceedings of logic in computer science, 72-81, (2005)
[12] M. Hofmann, T. Streicher, Continuation models are universal for \(\lambda \mu\)-calculus, in: Proc. the 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 387-395
[13] Hatcliff, J.; Sørensen, M.H., CPS-translation and applications: the cube and beyond, Higher-order and symbolic computation, 12, 2, 125-170, (1999) · Zbl 0936.03015
[14] Y. Lafont, B. Reus, T. Streicher, Continuation semantics or expressing implication by negation, Technical Report 93-21, University of Munich, 1993
[15] Löb, M.H., Embedding first order predicate logic in fragments of intuitionistic logic, The journal of symbolic logic, 41, 4, 705-718, (1976) · Zbl 0358.02012
[16] Murthy, C.R., Finding the answers in classical proofs: A unifying framework, (), 247-272
[17] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential type, ACM transactions on programming languages and systems, 10, 3, 470-502, (1988)
[18] Melton, A.; Schmidt, D.A.; Strecker, G.E., Galois connections and computer science applications, (), 299-312 · Zbl 0622.06004
[19] Nakazawa, K.; Tatsuta, M.; Kameyama, Y.; Nakano, H., Undecidability of type-checking in domain-free typed lambda-calculi with existence, (), 478-492 · Zbl 1156.03316
[20] Parigot, M., \(\lambda \mu\)-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[21] Plotkin, G., Call-by-name, call-by-value and the \(\lambda\)-calculus, Theoretical computer science, 1, 125-159, (1975) · Zbl 0325.68006
[22] Prawitz, D., Natural deduction, A proof theoretical study, (1965), Almqvist & Wiksell Stockholm · Zbl 0173.00205
[23] Priestley, H.A., Ordered sets and complete lattices, A primer for computer science, (), 21-78 · Zbl 1065.68036
[24] Reynolds, J.C., The discoveries of continuation, Lisp and symbolic computation, 6, 233-247, (1993)
[25] Sabry, A.; Felleisen, M., Reasoning about programs in continuation-passing style, Lisp and symbolic computation, 6, 289-360, (1993)
[26] Sabry, A.; Wadler, Ph., A reflection on call-by-value, ACM transactions on programming languages and systems, 19-6, 916-941, (1997)
[27] Selinger, P., Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical structures in computer science, 11, 207-260, (2001) · Zbl 0984.18003
[28] Streicher, Th.; Reus, B., Classical logic, continuation semantics and abstract machines, Journal of functional program, 8, 6, 543-572, (1998) · Zbl 0928.68074
[29] M. Tatsuta, K. Fujita, R. Hasegawa, H. Nakano, Inhabitation of existential types is decidable in negation-product fragment, in: Proc. Classical Logic and Computation, CLC2008, 2008
[30] Troelstra, A.S.; van Dalen, D., Constructivism in mathematics, an introduction, (1988), North-Holland · Zbl 0653.03040
[31] Ph. Wadler, Call-by-value is dual to call-by-name, in: International Conference on Functional Programming, August 25-29, Uppsala, 2003 · Zbl 1315.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.