---
title: "The System F of Variable Types, Fifteen Years Later"
authors:
  - "Jean-Yves Girard"
year: 1986
venue: "Theoretical Computer Science"
arxiv: null
doi: "10.1016/0304-3975(86)90044-7"
source: "https://doi.org/10.1016/0304-3975(86)90044-7"
topics:
  - system-f
  - girard
  - polymorphism
  - proof-theory
seed_rank: 639
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types"
    url: "https://doi.org/10.1016/S0049-237X(08)70843-7"
    year: 1971
    arxiv: null
    doi: "10.1016/S0049-237X(08)70843-7"
  - title: "Towards a Theory of Type Structure"
    url: "https://doi.org/10.1007/3-540-06859-7_148"
    year: 1974
    arxiv: null
    doi: "10.1007/3-540-06859-7_148"
see:
  - "638-girard-system-f-une-extension-de-linterpretation-de-godel"
  - "637-towards-a-theory-of-type-structure"
---

# The System F of Variable Types, Fifteen Years Later

## One-sentence takeaway

Girard’s 1986 retrospective gives the standard English presentation of System F — syntax, typing, candidates-of-reducibility, and the proof-theory-to-programming reading.

## Why it matters here

The System F paper most PL people actually cite. Pairs with TAPL’s polymorphism chapters and with Reynolds 1974/1983; this is the readable account of why impredicative ∀ normalizes.

## Key ideas

- Clean presentation of F’s syntax, typing rules, and β-reduction.
- Reducibility candidates prove strong normalization, hence consistency of second-order arithmetic.
- Connects the 1971 Dialectica-style origins to programming-language polymorphism (and to Reynolds’ independent discovery).
- *TCS* 45 (1986), pp. 159–192.

## Caveats

## Links

- DOI: [10.1016/0304-3975(86)90044-7](https://doi.org/10.1016/0304-3975(86)90044-7)