В докладе рассмотрены базовые понятия и ключевые результаты теории лямбда-исчисления: термы, нормализации, бета-редукция. теорема Черча-Россера. Особое внимание уделено связи лямбда-исчисления с теорией рекурсии. Так же будут рассмотрены простейшие способы типизации лямбда-исчисления: просто типизированное лямбда-исчисление, System T Гёделя. Представлен алгоритм foetus, позволяющий проверять, что программа завершает исполнение за конечное время на всех входах.