CPS-translation as adjoint

We show that there exist translations between polymorphic λ-calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic λ-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.