zbMATH — the first resource for mathematics

Galois embedding from polymorphic types into existential types. (English) Zbl 1114.03009
Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 194-208 (2005).
Summary: We show that there exist bijective translations between polymorphic \(\lambda\)-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.
For the entire collection see [Zbl 1070.03001].

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
Full Text: DOI