Спецификация чистой системы типов, правила и аксиомы типизации. Примеры PTS. Свойства PTS: редукция субъекта, лемма генерации, единственность типа. Сильная нормализуемость и разрешимость TCP и TSP. Населенность \( \bot \). Алгоритм синтеза типа для \( \lambda P \).