Avis des lecteurs
Résumé:Ce livre est considéré comme une introduction accessible aux types dépendants utilisant Agda, en particulier pour la démonstration pratique de théorèmes. Cependant, il présente des lacunes notables en termes de clarté, d'organisation et de présentation, ce qui nuit à son efficacité globale.
Avantages:L'introduction la plus accessible aux types dépendants dans la pratique, en particulier pour Agda.
Inconvénients:Prépare les lecteurs à des livres plus avancés sur le sujet.
(basé sur 4 avis de lecteurs)
Titre original :
Verified Functional Programming in Agda
Contenu du livre :
Agda est un langage de programmation avancé basé sur la théorie des types. Le système de types d'Agda est suffisamment expressif pour permettre une vérification fonctionnelle complète des programmes, dans deux styles.
Dans la vérification externe, nous écrivons des programmes fonctionnels purs, puis des preuves de leurs propriétés. Les preuves sont des artefacts externes distincts, utilisant typiquement l'induction structurelle. Dans la vérification interne, nous spécifions les propriétés des programmes par le biais de types riches pour les programmes eux-mêmes.
Cela nécessite souvent d'inclure des preuves à l'intérieur du code, pour montrer au vérificateur de type que les propriétés spécifiées sont valables. Le pouvoir de prouver les propriétés des programmes dans ces deux styles est un ajout profond à la pratique de la programmation, donnant aux programmeurs le pouvoir de garantir l'absence de bogues, et donc d'améliorer la qualité des logiciels plus qu'il n'était possible de le faire auparavant. La programmation fonctionnelle vérifiée en Agda est le premier livre à fournir une exposition systématique de la vérification externe et interne en Agda, adaptée aux étudiants de premier cycle en informatique.
Aucune familiarité avec la programmation fonctionnelle ou les preuves vérifiées par ordinateur n'est présupposée. Le livre commence par une introduction à la programmation fonctionnelle à travers des exemples familiers comme les booléens, les nombres naturels et les listes, et les techniques de vérification externe. La vérification interne est abordée à travers des exemples de vecteurs, d'arbres de recherche binaires et d'arbres de Braun.
Des éléments plus avancés sur le calcul au niveau du type, le raisonnement explicite sur la terminaison et la normalisation par évaluation sont également inclus. Le livre comprend également une étude de cas de taille moyenne sur le codage et le décodage de Huffman.
Autres informations sur le livre :
| ISBN : | 9781970001242 |
| Auteur : | |
| Éditeur : | |
| Reliure : | Broché |
Achat:
Actuellement disponible, en stock.
