Calculi with Second-Order Existential Quantifier

关于二阶存在型微积分的类型相关决策问题，我们得到了以下结果：(1)对于一些程序只包含部分类型信息的类型化λ微积分，我们证明了多态类型上的类型检查和可类型问题可以图灵约化为存在类型上的类型检查和可类型问题；(2)证明了存在类型片段的类型检查和可类型化问题之间的图灵等价，得到了存在类型无域λ演算中可类型化不可类型化的新证明；(3)证明了具有存在类型的无域微积分中的类型相关问题与具有多态类型的无域微积分中的类型相关问题之间的图灵等价。

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.