Guest
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: программирование в бестиповом лямбда-исчислении: представление булевых и арифметических функций; условный переход и кодирование пар; итерация; композиция и примитивная рекурсия сохраняют представимость; (первая) теорема о неподвижной точке; решение “уравнений“; явная рекурсия. ======== Если видео показалось вам полезным, вы можете поддержать автора: === If you have found this video helpful, you might want to support the author: === BTC: bc1q3p5x57cppjs0rfgj5f406yrljxylg96seed0t4
