Wprowadzenie do typów zależnych z Idris: kodowanie dowodów programu w typach

Opinie czytelników

Obecnie brak opinii czytelników. Ocena opiera się na 2 głosach.

Oryginalny tytuł:

Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

Zawartość książki:

Typy zależne to koncepcja, która pozwala programistom pisać kod przenoszący dowody. Idris to język programowania obsługujący typy zależne. Ta książka nauczy Cię matematycznych podstaw Idris, a także tego, jak używać go do pisania oprogramowania i matematycznego udowadniania właściwości.

Pierwsza część książki służy jako wprowadzenie do podstawowych teorii języka. Zaczyna się od przeglądu systemów formalnych i matematycznych systemów logicznych jako fundamentalnych bloków konstrukcyjnych, a następnie stopniowo przechodzi do typów zależnych. Następnie poznasz teorię typów dla typów zależnych. Następnie poznasz język programowania Idris, a na koniec zgłębisz tajniki systemów formalnych i sprawdzania typów poprzez ich implementację.

Wprowadzenie do typów zależnych z Idris przeprowadzi cię przez proste przykłady i bardziej zaawansowane techniki, zwiększając poziom trudności w miarę zdobywania wiedzy. Każdy rozdział zawiera zestaw ćwiczeń opartych na tym, co zostało w nim omówione, aby jeszcze bardziej ugruntować wiedzę. Nie jest wymagana specjalistyczna wiedza matematyczna wykraczająca poza podstawy, więc jest to idealne rozwiązanie dla początkujących.

Czego się nauczysz

Zrozumieć rachunek lambda i typy zależne.

⬤ Uzyskać wgląd w programowanie funkcyjne.

⬤ Pisz dowody matematyczne z Idrisem.

Dla kogo jest ta książka

Programiści, matematycy, pracownicy naukowi i wszyscy inni zainteresowani nauką typów zależnych i rachunku lambda.