• impredicativity
• Curry-Howard correspondence
• second-order logic

This thesis focuses on Girard/Reynolds system F, an extension of simply-typed lambda-calculus which can be treated as a prototypical programming language in the functional paradigm for polymorphism and as a computational interpretation of second-order (intuitionistic) logic and arithmetic. After a detailed exam of the expressive power of F, we present a reducibility argument for strong normalization of F (a result which is the Curry-Howard analogue of consistency for second-order intuitionistic logic and arithmetic). The realizability interpretation of F which stems from this argument is further refined, in order to obtain a non-circular reading of polymorphism (the Curry-Howard analogue of impredicative quantification) of autonomous philosophical interest. Turning attention to higher-order extensions of F, we show how to reformulate a positive solution to Takeuti's conjecture in Curry-Howard style, and how can we go paradoxical by admitting higher-order impredicativity. Particular emphasis is given to an (allegedly) original reformulation of Russell intensional paradox in an intuitionistic setting.