@techreport{oai:kyutech.repo.nii.ac.jp:00000685,
 author = {Fujita, Kenetsu and 藤田, 憲悦},
 month = {Jul},
 note = {We will prove that type checking, typability, and type inference fordomain-free  2 are undecidable. The type checking problem for domain-free  2 was posed by Barthe and S rensen (1997). A certain second or-der uni cation problem is reduced to the problem of type inference fordomain-free  2. The restricted second order uni cation has been provenundecidable by Schubert. The reduction method can be obtained from asimpli cation of Pfenning's reduction from the general problem of secondorder uni cation to the partial type inference problem. An analysis of theundecidability proof reveals that the typability problem is still undecid-able even for a predicative fragment of domain-free 2, called the rank 2fragment.},
 title = {Type Inference for Domain-Free λ2},
 year = {1999},
 yomi = {フジタ, ケンエツ}
}