Introducere în tipurile dependente cu Idris: Codificarea probelor de program în tipuri

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 2 voturi.

Titlul original:

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

Conținutul cărții:

Tipurile dependente sunt un concept care le permite dezvoltatorilor să scrie coduri care suportă dovezi. Idris este un limbaj de programare care acceptă tipuri dependente. Această carte vă va învăța bazele matematice ale Idris, precum și cum să îl utilizați pentru a scrie software și pentru a demonstra matematic proprietăți.

Prima parte a cărții servește ca o introducere în teoriile care stau la baza limbajului. Începe prin trecerea în revistă a sistemelor formale și a sistemelor logice matematice ca elemente de bază, apoi se construiește treptat până la tipurile dependente. În continuare, veți învăța teoria tipurilor pentru tipurile dependente. În continuare, veți explora limbajul de programare Idris și veți încheia prin a explora profunzimea sistemelor formale și a verificatoarelor de tip prin implementarea acestora.

Introducere în tipurile dependente cu Idris vă va ghida prin exemple simple până la tehnici mai avansate, crescând gradul de dificultate pe măsură ce veți dobândi mai multe cunoștințe. Fiecare capitol include un set de exerciții bazate pe ceea ce a acoperit pentru a vă cimenta în continuare învățarea. Nu se așteaptă cunoștințe specializate de matematică dincolo de elementele de bază, deci este perfect pentru începători.

Ce veți învăța

Înțelegeți calculul Lambda și tipurile dependente.

⬤ Obțineți o perspectivă asupra programării funcționale.

⬤ Scrie demonstrații matematice cu Idris.

Pentru cine este această carte

Programatori, matematicieni, academicieni și oricine altcineva interesat să învețe tipuri dependente și lambda calculus.