---
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"
authors:
  - "Jean-Yves Girard"
year: 1971
venue: "Proceedings of the Second Scandinavian Logic Symposium"
arxiv: null
doi: "10.1016/S0049-237X(08)70843-7"
source: "https://doi.org/10.1016/S0049-237X(08)70843-7"
topics:
  - system-f
  - girard
  - proof-theory
  - polymorphism
seed_rank: 638
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites: []
see: []
---

# 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

## One-sentence takeaway

Girard extends Gödel’s Dialectica interpretation to second-order arithmetic and, in doing so, introduces System F — the second-order λ-calculus — with a strong-normalization / cut-elimination proof.

## Why it matters here

The proof-theoretic twin of Reynolds polymorphism. Essential for connecting type theory to logic on Broadside’s maths/PL shelf, and the reason System F is known to normalize (so polymorphic ano terms cannot loop just by being polymorphic).

## Key ideas

- System F / λ2 arises as the functional interpretation of second-order (impredicative) arithmetic.
- Strong normalization of F yields cut-elimination for second-order logic / analysis.
- Impredicative polymorphism: a type variable ranges over all types, including those that quantify.
- *Proc. 2nd Scandinavian Logic Symposium* (Studies in Logic 63), North-Holland, 1971. The 1986 TCS retrospective (639) is the readable English account.

## Caveats

## Links

- DOI: [10.1016/S0049-237X(08)70843-7](https://doi.org/10.1016/S0049-237X(08)70843-7)