Angiuli C., Gratzer D., Principles of Dependent Type Theory.
Организатор: @GabrielFallen

Начинаем читать учебник по теориям типов для студентов. На первой встрече обсудим первый раздел, «Введение». Он короткий и носит мотивирующий характер, но тем не менее обращает внимание на ряд существенных вопросов:
— типы, актуально зависящие от значений и их необходимость
— разница между вычислением закрытых термов и редукцией открытых
— разница между definitional equality и propositional equality.

Приглашаются все, кто интересуется теорией типов, как со стороны программирования, так и со стороны формальной логики и теории категорий.

Прочитать Introduction к воскресенью, 5 июля. Встречаемся на нашем дискорд-сервере в 16:00 по Москве.

Книга в первом комменте.
Формат | Методы доступа в дискорд