Galois embedding from universal types into existential types Extended Abstract -

摘要

We- show ilmi. there exist translations between polymorphic A-calculus and a .subsystem of niinitiml logic, with existential types, which form a (minis insertion (embedding). Froia a programming point of view, this result means that' abstract ilat-H types am interpret polymorphic functions under OPS-translation.