Bewertung:
Derzeit gibt es keine Leserbewertungen. Die Bewertung basiert auf 3 Stimmen.
Lambda Calculus with Types
Dieses Handbuch mit Übungen offenbart in Formalismen, die bisher hauptsächlich für den Entwurf und die Verifikation von Hard- und Software verwendet wurden, unerwartete mathematische Schönheit. Der Lambda-Kalkül bildet den Prototyp einer universellen Programmiersprache, die in ihrer untypisierten Version mit Lisp verwandt ist und in dem Klassiker The Lambda Calculus (1984) des ersten Autors behandelt wurde.
Der Formalismus wurde seither um Typen erweitert und in der funktionalen Programmierung (Haskell, Clean) und in Beweisassistenten (Coq, Isabelle, HOL) verwendet, die beim Entwurf und der Überprüfung von IT-Produkten und mathematischen Beweisen zum Einsatz kommen. In diesem Buch konzentrieren sich die Autoren auf drei Klassen von Typisierungen für Lambda-Terme: einfache Typen, rekursive Typen und Schnittpunkttypen.
Es sind diese drei Formalismen für Terme und Typen, die die unerwartete mathematische Schönheit offenbaren. Es handelt sich um eine maßgebliche und umfassende Abhandlung, die durch eine ausführliche Bibliographie ergänzt wird, und es werden zahlreiche Übungen angeboten, um das Verständnis der Leser zu vertiefen und ihre Sicherheit im Umgang mit Typen zu erhöhen.
| ISBN: | 9780521766142 |
| Autor: | |
| Verlag: | |
| Einband: | Hardcover |
| Erscheinungsjahr: | 2013 |
| Seitenzahl: | 856 |
Derzeit verfügbar, auf Lager.
