Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в $ \lambda2 $. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы.