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