Курсът въвежда студентите в основите на ламбда смятането и структурната теория на формалните доказателства, като акцентира върху тясната връзка между тези две области на математическата логика. В първата част от лекциите се разглеждат нетипизираното и типизираното ламбда смятане като модели за описване на формални изчисления чрез функционални програми. Разглеждат се основни резултати, свързани с правилата за редукция, като конфлуентност, силна нормализация (в случая на типизирано смятане) и съществуване на безкрайни редукции (в случая на нетипизирано смятане). Втората част от лекциите започва с базовата идея за разглеждане на доказателството като абстрактен обект и описва основните типове системи за представяне на формални доказателства. Първоначално се разглеждат чисто логически системи, като се набляга на разликата между минимална, конструктивна и класическа логика и се описва близкото съответствие между типизирано λ-смятане и системи за естествен извод. Отделя се внимание на основния резултат за силна нормализация в контекста на системи за естествен извод. В последната част от курса се разглеждат аритметични системи, базирани на системи с крайни типове от произволен ред с примитивна рекурсия (система Т на Гьодел). Обръща се внимание на практическите аспекти на теорията: автоматична проверка и обработка на доказателства, извличане на програми от конструктивни доказателства чрез интерпретация за реализуемост.