![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
автоматический доказатель
Jan. 21st, 2011 08:02 pmПосле нового года опять заработал мехматовский семинарчик по логике. Сейчас Женя Беркович на доске программирует в примитивно-рекурсивных функциях лямбда-исчисление. Доказывает, что они эквивалентны. Можно подумать кто-то сомневался. Но есть же любители.
В перерывах между смотрением на доску, скачал книгу Logic in Computer Science 2nd - Huth & Ryan.PDF. Я под впечатлением от открытия для себя изоморфизма Кари-Говарда, автоматического доказателя теорем Coq, а так же созданного с его помощью формально доказанного компилятора Compsert. Жду не дождусь, когда компьютеры заменят программистов.
В перерывах между смотрением на доску, скачал книгу Logic in Computer Science 2nd - Huth & Ryan.PDF. Я под впечатлением от открытия для себя изоморфизма Кари-Говарда, автоматического доказателя теорем Coq, а так же созданного с его помощью формально доказанного компилятора Compsert. Жду не дождусь, когда компьютеры заменят программистов.
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif){kind=small}
