С.Л. Кузнецов. Спецкурс «Лямбда-исчисление, или вычислительная теория доказательств»