Интерпретация высказывания-как-типы. Правильность и полнота представления. Прямое представление логик в системах лямбда-куба. Logical Framework: представление различных логик в \( \lambda P \).