Bewertung:
Derzeit gibt es keine Leserbewertungen. Die Bewertung basiert auf 2 Stimmen.
Introduction to Dependent Types with Idris: Encoding Program Proofs in Types
Abhängige Typen sind ein Konzept, das es Entwicklern ermöglicht, beweiskräftigen Code zu schreiben. Idris ist eine Programmiersprache, die abhängige Typen unterstützt. In diesem Buch lernen Sie die mathematischen Grundlagen von Idris kennen und erfahren, wie Sie mit Idris Software schreiben und Eigenschaften mathematisch beweisen können.
Der erste Teil des Buches dient als Einführung in die der Sprache zugrunde liegenden Theorien. Zunächst werden formale Systeme und mathematisch-logische Systeme als grundlegende Bausteine besprochen, um dann schrittweise zu abhängigen Typen überzugehen. Als nächstes lernen Sie die Typentheorie für abhängige Typen kennen. Im Anschluss daran lernen Sie die Programmiersprache Idris kennen und erkunden abschließend die Tiefen formaler Systeme und Typprüfungen, indem Sie diese implementieren.
Einführung in abhängige Typen mit Idris führt Sie durch einfache Beispiele bis hin zu fortgeschrittenen Techniken und steigert den Schwierigkeitsgrad mit zunehmendem Wissen. Jedes Kapitel enthält eine Reihe von Übungen, die auf dem behandelten Thema basieren, um das Gelernte weiter zu festigen. Über die Grundlagen hinaus werden keine speziellen Mathematikkenntnisse erwartet, so dass das Buch auch für Anfänger geeignet ist.
(Was Sie lernen werden)
Verstehen des Lambda-Kalküls und abhängiger Typen.
⬤ Einblick in die funktionale Programmierung.
⬤ Schreiben Sie mathematische Beweise mit Idris.
Für wen ist dieses Buch gedacht?
Programmierer, Mathematiker, Akademiker und alle anderen, die abhängige Typen und Lambda-Kalkül lernen wollen.
| ISBN: | 9781484292587 |
| Autor: | |
| Verlag: | |
| Sprache: | Englisch |
| Einband: | Taschenbuch |
| Erscheinungsjahr: | 2023 |
| Seitenzahl: | 157 |
Derzeit verfügbar, auf Lager.
