原子多态中的可类型化性与类型推断
Typability and Type Inference in Atomic Polymorphism
AI总结：
本文研究系统Fat的Curry风格变体，证明可类型化性可判定，并提出能处理非冗余约束的类型推断算法。
摘要：
众所周知，在Girard-Reynolds多态系统F中，可类型化性、类型居留和类型推断是不可判定的。最近已证明，即使在系统F的谓词片段中，所有全称实例化都具有原子见证（系统Fat），类型居留仍然不可判定。本文分析了系统Fat的Curry风格变体中的可类型化性和类型推断，并表明可类型化性是可判定的，且存在一种能够处理非冗余约束的类型推断算法。
英文摘要：
It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fat and show that typability is decidable and that there is an algorithm for type inference which is capable of dealing with non-redundancy constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
