Bewertung:
Die Rezensionen des Buches heben die Zugänglichkeit und die praktische Herangehensweise an abhängige Typen unter Verwendung von Agda hervor und betonen die Eignung des Buches für Anfänger trotz einiger Mängel in der Klarheit und Organisation. Während viele Leser das Buch als exzellent zum Erlernen von Agda und Theorembeweisen empfinden, gibt es Kritik an seiner Struktur, Klarheit und Präsentation, insbesondere in der Kindle-Version.
Vorteile:⬤ Zugängliche Einführung in abhängige Typen in praktischen Situationen unter Verwendung von Agda.
⬤ Bereitet den Leser auf fortgeschritteneres Material zur Typentheorie und zum Theorembeweisen vor.
⬤ Enthält eine große Anzahl von einfachen Beweisen und praktischen Beispielen.
⬤ Geeignet für Leser ohne Vorkenntnisse in Logik oder Typentheorie, was die Reichweite des Buches erhöht.
⬤ Fehlt die theoretische Behandlung von abhängigen Typen.
⬤ Einige Abschnitte betonen nicht die großen Konzepte, bevor sie ins Detail gehen.
⬤ Einige Punkte werden übermäßig wiederholt, während andere nur unzureichend erklärt werden.
⬤ Die Kindle-Version hat ein schlechtes Layout, mit unzureichender Einrückung der Absätze und Ausrichtungsproblemen mit dem Quellcode.
(basierend auf 4 Leserbewertungen)
Verified Functional Programming in Agda
Agda ist eine fortgeschrittene Programmiersprache, die auf der Typentheorie basiert. Das Typensystem von Agda ist ausdrucksstark genug, um eine vollständige funktionale Verifikation von Programmen in zwei Varianten zu unterstützen.
Bei der externen Verifikation schreiben wir reine funktionale Programme und schreiben dann Beweise für Eigenschaften über sie. Die Beweise sind separate externe Artefakte, typischerweise unter Verwendung struktureller Induktion. Bei der internen Verifikation spezifizieren wir die Eigenschaften von Programmen durch umfangreiche Typen für die Programme selbst.
Dazu ist es oft notwendig, Beweise in den Code einzubauen, um dem Typ-Prüfer zu zeigen, dass die angegebenen Eigenschaften zutreffen. Die Möglichkeit, Eigenschaften von Programmen auf diese beiden Arten zu beweisen, ist eine tiefgreifende Bereicherung der Programmierpraxis, da sie dem Programmierer die Möglichkeit gibt, die Abwesenheit von Fehlern zu garantieren und damit die Qualität der Software mehr als bisher zu verbessern. Verified Functional Programming in Agda ist das erste Buch, das eine systematische Darstellung der externen und internen Verifikation in Agda bietet und für Studenten der Informatik im Grundstudium geeignet ist.
Es wird keine Vertrautheit mit funktionaler Programmierung oder computergeprüften Beweisen vorausgesetzt. Das Buch beginnt mit einer Einführung in die funktionale Programmierung anhand von bekannten Beispielen wie Booleschen Zahlen, natürlichen Zahlen und Listen sowie Techniken zur externen Verifikation. Die interne Verifikation wird am Beispiel von Vektoren, binären Suchbäumen und Braun-Bäumen betrachtet.
Weiteres Material über Berechnungen auf Typebene, explizite Schlussfolgerungen über die Beendigung und Normalisierung durch Auswertung ist ebenfalls enthalten. Das Buch enthält auch eine mittelgroße Fallstudie zur Huffman-Kodierung und -Dekodierung.
| ISBN: | 9781970001273 |
| Autor: | |
| Verlag: | |
| Sprache: | Englisch |
| Einband: | Hardcover |
Derzeit verfügbar, auf Lager.
