F系統（也稱多態λ微積分或二階λ微積分）是一種類型化的λ微積分，它在簡單的類型化λ微積分中引入了一種對類型進行普遍量化的機制。F系統將編程語言中的參數多態性正式化，從而形成了諸如Haskell和ML等語言的理論基礎。它是由邏輯學家Jean-YvesGirard（1972）和計算機科學家JohnC.Reynolds（1974）獨立發現的。簡單類型的lambdacalculus的變量范圍是術語，并為它們提供了綁定器，而SystemF的變量范圍是類型，并為它們提供了綁定器。例如，身份函數可以有A→A形式的任何類型，這一事實在系統F中被形式化為判斷傳統上用于表示類型級函數，而小寫的則是{displaystylelambda}，后者用于表示值級函數。它用于表示值級函數。(上標的{displaystylealpha}意味著邊界x是一種類型。意味著邊界x的類型是{displaystyle`alpha}；冒號后面的表達式是前面的λ表達式的類型。冒號后面的表達式是它前面的λ表達式的類型）。作為一個術語重寫系統，SystemF是強規范化的。

然而，F系統中的類型推理（沒有明確的類型注釋）是不可判定的。在Curry-Howard同構下，F系統對應于二階直覺邏輯的片段，該片段只使用普遍量化。系統F可以被看作是lambdacube的一部分，同時還有更具表現力的類型化lambda計算，包括那些具有依賴類型的計算。根據Girard的說法，系統F中的F是偶然被選中的。

F系統的類型化規則是那些簡單類型化λ計算的規則，并增加了以下內容。是綁定的。xxx個規則是應用的規則，第二個規則是抽象的規則。邏輯和謂詞The{displaystyle{mathsf{Boolean}}是所有函數的類型，這些函數的輸入是一個類型α和兩個類型α的表達式。｝是所有函數的類型，這些函數將一個類型α和兩個類型α的表達式作為輸入，并將一個類型α的表達式作為輸出(注意，以上兩個函數需要三個--而不是兩個--參數。后兩個應該是lambda表達式，但xxx個應該是一個類型。這一事實反映在這些表達式的類型是?α.α→α→α{displaystyleforallalpha.alphatoalphaalpha}。；綁定α的通用量詞對應于λ表達式本身中綁定α的Λ。另外，請注意也是F系統組合的元符號，方便的速記符號（在布爾巴基的意義上）；否則，如果這些函數可以被命名（在F系統內），那么就不需要能夠匿名定義函數的λ表達式裝置，也不需要繞過這一限制的定點組合器了）。