System F is a type system historically developed independently by Jean-Yves Girard and John Reynolds. It enriches simply typed lambda calculus with an impredicative universal quantifier over types.

Logically, it corresponds to second order minimal logic, that is, a second order logic without first-order quantifiers. The idea of having second order quantifications, but not first order ones, stems from the observation that first order quantiication doesn’t have a clear computational interpretation.