Girard, Jean-Yves 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.(An extension of Gödel’s interpretation to analysis and its application to cut elimination in analysis and type theory). (French) Zbl 0221.02013 Proc. 2nd Scandinav. Logic Sympos. 1970, Studies Logic Foundations Math. 63, 63-92 (1971). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 5 ReviewsCited in 10 Documents MSC: 03F03 Proof theory in general (including proof-theoretic semantics) 03F10 Functionals in proof theory 03B15 Higher-order logic; type theory (MSC2010) 03F25 Relative consistency and interpretations PDF BibTeX XML OpenURL