Introduction aux types dépendants avec Idris - Apprendre les preuves de programmes en types

Introduction aux types dépendants avec Idris : encoder des preuves de programmes dans des types (Boro Sitnikovski)

Avis des lecteurs

Il n'y a actuellement aucun avis de lecteur. La note est basée sur 2 votes.

Titre original :

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

Contenu du livre :

Les types dépendants sont un concept qui permet aux développeurs d'écrire du code porteur de preuves. Idris est un langage de programmation qui prend en charge les types dépendants. Ce livre vous apprendra les fondements mathématiques d'Idris ainsi que la manière de l'utiliser pour écrire des logiciels et prouver mathématiquement des propriétés.

La première partie du livre sert d'introduction aux théories sous-jacentes du langage. Elle commence par passer en revue les systèmes formels et les systèmes logiques mathématiques en tant que blocs de construction fondamentaux, puis s'étend progressivement jusqu'aux types dépendants. Ensuite, vous apprendrez la théorie des types pour les types dépendants. Ensuite, vous explorerez le langage de programmation Idris et conclurez en explorant les profondeurs des systèmes formels et des vérificateurs de type en les implémentant.

Introduction aux types dépendants avec Idris vous guidera à travers des exemples simples jusqu'à des techniques plus avancées, en augmentant la difficulté au fur et à mesure que vous acquerrez plus de connaissances. Chaque chapitre comprend une série d'exercices basés sur ce qu'il a couvert afin de cimenter davantage votre apprentissage. Aucune connaissance spécialisée en mathématiques n'est attendue au-delà des bases, ce cours est donc parfait pour les novices.

Ce que vous apprendrez

Comprendre le calcul Lambda et les types dépendants.

⬤ Comprendre la programmation fonctionnelle.

⬤ Écrire des preuves mathématiques avec Idris.

A qui s'adresse ce livre ?

Programmeurs, mathématiciens, universitaires et toute personne intéressée par l'apprentissage des types dépendants et du lambda calcul.