System F – jeden z wariantów rachunku lambda z typami. Jest to najprostszy rachunek zawierający typy proste oraz typy polimorficzne.

Zbiór typów można zdefiniować jako najmniejszy taki zbiór U, że przy danym, ustalonym i przeliczalnym zbiorze zmiennych V, zachodzą następujące własności:

• V zawiera się w U,
• jeśli ${\displaystyle \sigma }$ oraz ${\displaystyle \tau }$ należą do U, to ${\displaystyle \sigma \to \tau }$ również należy do U,
• jeśli ${\displaystyle \alpha }$ jest zmienną (należy do V) oraz ${\displaystyle \sigma }$ należy do U, to ${\displaystyle \forall \alpha .\ \sigma }$ również należy do U.

Typy postaci ${\displaystyle \forall \alpha .\ \sigma }$ należy traktować (nieformalnie) jako każdą możliwą instancję typu ${\displaystyle \sigma }$ taką, że za każde wystąpienie zmiennej ${\displaystyle \alpha }$ wstawiamy dowolny inny typ (za każde wystąpienie zmiennej ten sam).