Bevezetés a függő típusokba Idris-szel: Programbizonyítások kódolása típusokba

Olvasói vélemények

Jelenleg nincsenek olvasói vélemények. Az értékelés 2 olvasói szavazat alapján történt.

Eredeti címe:

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

Könyv tartalma:

A függő típusok egy olyan koncepció, amely lehetővé teszi a fejlesztők számára, hogy bizonyító erejű kódot írjanak. Az Idris egy olyan programozási nyelv, amely támogatja a függő típusokat. Ez a könyv megtanítja az Idris matematikai alapjait, valamint azt, hogyan használjuk szoftverek írására és tulajdonságok matematikai bizonyítására.

A könyv első része bevezetésként szolgál a nyelv mögöttes elméleteibe. A formális rendszerek és a matematikai logikai rendszerek, mint alapvető építőelemek áttekintésével kezdődik, majd fokozatosan építkezik a függő típusokig. Ezután a függő típusok típuselméletét tanulja meg. Ezt követően az Idris programozási nyelvvel ismerkedik meg, majd befejezésül a formális rendszerek és a típusellenőrzők mélységeit tárja fel azok megvalósításával.

A Bevezetés a függő típusokba Idris-szel egyszerű példákon keresztül vezet végig a fejlettebb technikákon keresztül, a nehézségeket a tudás bővülésével fokozva. Minden fejezet tartalmaz egy sor feladatot a tárgyalt témák alapján, hogy tovább szilárdítsa a tanulást. Az alapokon túl nem várható el speciális matematikai tudás, így a könyv tökéletes kezdők számára.

Mit fogsz tanulni

Megérti a Lambda-számítást és a függő típusokat.

⬤  Betekintést nyerhet a funkcionális programozásba.

⬤ Írd a matematikai bizonyításokat Idrisszel.

Kinek szól ez a könyv

Programozóknak, matematikusoknak, akadémikusoknak és bárkinek, aki érdeklődik a függő típusok és a lambda-számítás megismerése iránt.