System F

• Second-order propositional logic
• Polymorphism
• System F: terms and typing rules
• Encoding pairs, sums and bottom.
• Strong normalization proof.