Лялямбда

школа верификации, компиляторов и реверса

'21

с элементами прикладного ФП

17-07—01/08

Участникам

Летняя школа Лялямбда-2021 пройдёт с 17 июля по 1 августа в Парк-отеле Ершово (Московская обл., Одинцовский г.о., с. Ершово, кв-л Дома отдыха Ершово, стр.22). Наша группа проживает в корпусе №3. В стоимость проживания включено трёхразовое питание по системе шведский стол, в стоимость оргсбора включены полдники и вечерние перекусы на свечке.

Нами запланирован организованный трансфер:

• туда 17 июля утром (суббота)
• туда 24 июля утром (суббота)
• обратно 28 июля вечером (среда)
• обратно 1 августа вечером (воскресенье)

Материалы пре-школы

К школе можно подтянуть свои знания, пройдясь по указанным ниже методичкам. По ходу можно задавать вопросы в чате участников, кто-нибудь обязательно подскажет.

• Как делать воркшопы

ФП

• Курс Москвина про Haskell

Coq

• Курс Антона по Coq (+лекции на YouTube)

• Logical Foundations (+лекции (“Coq intensive”) с DSSS)

TLA

• Книга Specifying Systems и упражнения к ней
• Лекции Лампорта

Подготовка ЭВМ

Тестовые программы для проверки окружения: https://git.sr.ht/~omrigan/lalambda-env.

Coq

• Дима советует: заведите VSCode + VSCoq.
• Антон советует: пользуйте Emacs + Proof General.
• Олег бурчит: если ничего не работает, сработает CoqIDE из Coq platform.

TLA+

Установите Java 16 и TLA+ Toolbox.

Haskell

Установите Stack и запустите stack ghci.