Functional Data Structures and Algorithms: a Proof Assistant Approach
Книга вводит структуры данных и алгоритмы для функциональных языков с акцентом на доказательства. Она охватывает функциональную корректность и анализ времени выполнения в едином подходе: индуктивные доказательства применяются как к самим программам, так и к их функциям времени. Подходит для изучения в функциональном стиле, с примерами и полными формальными проверками.
Все доказательства machine-checked в доказательном ассистенте Isabelle; PDF-версия содержит гиперссылки на соответствующие теории Isabelle для самостоятельной верификации. Книга открыта для эволюции — авторы приглашают к вкладу и совместной доработке. Доступны изображения обложки и содержания для скачивания полного PDF.