Доказательства на разные темы, разбор необходимости проверок структурной рекурсии, строгой позитивности, исключение Type:Type
Введение в формальную верификацию программ