Pure type systems

• Sorts
• Pure type systems
• Lambda cube
• Calculus of constructions