Calculi with Second-Order Existential Quantifier

点击翻译按钮获取中文摘要

We have got the following results on some type-related decision problems of calculi with second-order existential types :(1) for some typed lambda calculi where programs contain only partial type information, we have proved that type-checking and typability problems on polymorphic types are Turing reducible to those on existential types, and we have shown that those problems on existential types are undecidable,(2) we have proved the Turing equivalence between type-checking and typability problems in some fragments with existential type, and we have got new proofs of undecidability of typability in the domain-free lambda calculi with existential types, and(3) we have proved the Turing equivalence between the type-related problems in domain-free calculi with existential types and those in domain-free calculi with polymorphic types.