Формальное доказательство эквивалентности программ, скомпилированных в ABI со статическим и динамическим связыванием
Осторожно, сабмодули! Не забывайте скармливать ключ --recursive при
клонировании репозитория.
В каталоге build находятся скомпилированные pdf-ки с презентацией и
пояснительной запиской. В презенташке достаточно обзорно рассказано, что и
как я делаю и какие результаты я получаю, а еще там есть некоторый текст
про то, как полученный результат свести к указанной теме работы (в
пояснительной записке этого нет). За более подробной информацией необходимо
уже лезть в пояснительную записку.
Альтернативный способ чтения пояснительной записки - открывать исходник
третьей главы (agda/Functions.lagda) в emacs и там читать, используя
преимущества интерактивного взаимодействия с Agda.
Для сборки необходимы:
graphvizimagemagickagdapandocxelatexbibtex
... и некоторый набор стандартных утилит.
В корневом Makefile есть два главных интересных таргета (кроме очевидного
all): report и slides для пояснительной записки и презентации
соответственно.
Энджой.