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