System Fω

• Kinds
• Type-level abstraction and application
• Strong normalization proof