Kalkulator lambda z typami

Opinie czytelników

Obecnie brak opinii czytelników. Ocena opiera się na 3 głosach.

Oryginalny tytuł:

Lambda Calculus with Types

Zawartość książki:

Ten podręcznik z ćwiczeniami ujawnia w formalizmach, dotychczas używanych głównie do projektowania i weryfikacji sprzętu i oprogramowania, nieoczekiwane matematyczne piękno. Rachunek lambda jest prototypem uniwersalnego języka programowania, który w wersji bez typów jest spokrewniony z Lispem i został omówiony w klasycznym The Lambda Calculus (1984) pierwszego autora.

Od tego czasu formalizm został rozszerzony o typy i wykorzystany w programowaniu funkcjonalnym (Haskell, Clean) i asystentach dowodu (Coq, Isabelle, HOL), wykorzystywanych w projektowaniu i weryfikacji produktów informatycznych i dowodów matematycznych. W niniejszej książce autorzy skupiają się na trzech klasach typowania wyrażeń lambda: typach prostych, typach rekurencyjnych i typach przecięcia.

To właśnie w tych trzech formalizmach terminów i typów ujawnia się nieoczekiwane matematyczne piękno. Opracowanie jest autorytatywne i kompleksowe, uzupełnione wyczerpującą bibliografią, a liczne ćwiczenia mają na celu pogłębienie zrozumienia przez czytelników i zwiększenie ich pewności siebie w posługiwaniu się typami.