Typability and type checking in System F are equivalent and undecidable

This publication has 28 references indexed in Scilit:

• The emptiness problem for intersection types
  The Journal of Symbolic Logic, 1999
• Type reconstruction in F_ω
  Mathematical Structures in Computer Science, 1997
• A direct algorithm for type inference in the rank-2 fragment of the second-order λ-calculus
  ACM SIGPLAN Lisp Pointers, 1994
• The complexity of type inference for higher-order typed lambda calculi
  Journal of Functional Programming, 1994
• Type reconstruction in finite rank fragments of the second-order λ-calculus
  Information and Computation, 1992
• Polymorphic type inference and containment
  Information and Computation, 1988
• The undecidability of the second-order unification problem
  Theoretical Computer Science, 1981
• The Principal Type-Scheme of an Object in Combinatory Logic
  Transactions of the American Mathematical Society, 1969
• The undecidability of the Turing machine immortality problem
  The Journal of Symbolic Logic, 1966
• Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines
  Annals of Mathematics, 1961