Linear logic

Girard, 1971, Une extension de l'interprétation de Gödel à l'analyse et son application à l'elimination des coupures dans l'analyse et dans la théorie des types, 63

Girard, 1972, Interprétation fonctionelle et élimination des cupures de l'arithmétique d'ordre supérieur

Girard, 1976, Three-valued logic and cut-elimination: the actual meaning of Takeuti's conjecture, Dissertationes Math., CXXXVI

J.-Y. Girard, Normal functors, power series and lambda-calculus, Ann. Pure Appl. Logic, to appear.

Girard, 1986, The system F of variable types, Theoret. Comput. Sci., 45, 159, 10.1016/0304-3975(86)90044-7

Kreisel, 1974, Formally self-referential propositions for cut-free classical analysis and related systems, Dissertationes Math., CXVIII