tgoop.com/noml_digest/797
Last Update:
Про теорию типов
В завершение темы прошлой недели подборка материалов от Дмитрия Штукенберга.
Введение в основания математики
▫️ S.C. Kleene, Introduction to Metamathematics, 1952 (перевод: С.К. Клини, Введение в метаматематику, 1957) (~550 стр.)
Теория типов
▫️ Хорошее введение в тему: интуиционисткая логика, изоморфизм Карри-Ховарда, линейная логика и как всё это связано с функциональным программированием: P. Wadler, A Taste of linear Logic, 1993 (27 стр.)
▫️ Здесь в целом про конструктивную математику для программирования: P. Martin-Löf, Constructive mathematics and computer programming, 1982 (23 стр.)
▫️ Гомотопическая теория типов (HoTT) и вообще один из современных взглядов в сторону оснований математики, плюс в первой главе хорошее введение в целом в теорию типов: Homotopy Type Theory: Univalent Foundations of Mathematics, 2013 (перевод) (475 стр.)
На ресурсе homotopytypetheory.org можно найти много других материалов про HoTT.
Языки и инструменты
▫️ Coq / Rocq
Плюс учебник: A. Chipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013–2019 (~400 стр.)
▫️ Agda
▫️ F* (F star)
▫️ Arend
И список библиотек и расширений на базе HoTT
Пара интересных приложений
▫️ Задача о четырёх красках: G. Gonthier, A computer-checked proof of the Four Colour Theorem, 2005 (57 стр.)
▫️ Верификатор для Solidity: coq-of-solidity
BY NoML Digest
Share with your friend now:
tgoop.com/noml_digest/797