Girard and Reynolds independently invented System F to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates types with untyped lambda terms, raises the questions of typability and type checking. Typability asks for a term whether there exists some type it can be given. Type checking asks, for a particular term and type, whether the term can be given that type. The decidability of these problems has been settled for restrictions and (...) extensions of F and related systems and complexity lower-bounds have been determined for typability in F, but this report is the first to resolve whether these problems are decidable for System F. This report proves that type checking in F is undecidable, by a reduction from semi-unification, and that typability in F is undecidable, by a reduction from type checking. Because there is an easy reduction from typability to type checking, the two problems are equivalent. The reduction from type checking to typability uses a novel method of constructing lambda terms that simulate arbitrarily chosen type environments. All of the results also hold for the λI-calculus. (shrink)

Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions.It covers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new result.Finally, the relation to Parigot’s strictly positive inductive definition of his set of reducibility candidates and to his notion of generalized reducibility candidates is explained.