A._J.__Kfoury
A direct algorithm for type inference in the rank 2 fragment of the second-order lambda-calculus
A direct algorithm for type inference in the rank-2 fragment of the second-order ??-calculus
Addendum to "New notions of reduction and non-semantic proofs of fi-strong normalization in typed -calculi
Beta-reduction as unification
New Notions of Reduction and Non-Semantic Proofs of Beta Strong Normalization in Typed Lambda Calculi
Principality and decidable type inference for finite-rank intersection types
Type reconstruction in the presence of polymorphic recursion