Wszystko zależy od tego, jak głęboko chcesz zejść i ile już wiesz. Dla początkującego książka Winksel jest naprawdę fajna, ale tak, nie wprowadza cię w stan semantyki, jak napisano około 20 lat temu. Niemniej jednak jest to dobre pierwsze wprowadzenie do tematu. Warto również wskazać, że T. Nipkow sformalizował znaczną część książki Winskela w Isabelle / HOL, patrz tutaj . Jeśli więc chcesz nauczyć się korzystać z interaktywnych asystentów sprawdzających wraz ze zrozumieniem semantyki języków programowania, masz wiele spójnych materiałów do wykorzystania.
Inne bardziej zaawansowane książki to:
Gunter, Semantyka języków programowania , bardziej zaawansowana książka skupiająca się na semantyce denotacyjnej, podejściu do semantyki, która nie spełniła oczekiwań. Koncentruje się na czysto funkcjonalnych językach i ignoruje współbieżność. Jest to książka, od której nauczyłem się semantyki jako licencjat, i z perspektywy czasu żałuję, że nie zamiast tego użyłem książki Winksel. Gunter nie jest łatwym do przeczytania dla początkującego.
Domeny i rachunek lambda Amadio i Curien. Kolejna książka, napisana bardziej w tradycji teoretycznej, choć omawia rachunek procesowy.
Książki Johna Mitchella, które zostały już wspomniane powyżej. Dotyczą one głównie obliczeń sekwencyjnych.
Książki takie jak TAPL Pierce'a są bardzo ładne, ale skupiają się wąsko na jednym aspekcie języków programowania, a mianowicie na typach, tak samo ważnych. Nie polecałbym tego jako pierwszego wprowadzenia do ogólnej dziedziny języków programowania, ale jest to obowiązkowe lektury dla każdego, kto chce dowiedzieć się o typach.
Prawdę mówiąc, myślę, że obecnie nie ma aktualnej książki wprowadzającej na temat semantyki języka, która odzwierciedla znaczny postęp, jaki nastąpił w ostatniej dekadzie, z jej zdecydowanym przejściem od metod denotacyjnych i obliczeń sekwencyjnych do współbieżności (kalkulacja procesów i semantyka gry) , semantyka aksjomatyczna i zastosowanie interaktywnych asystentów dowodowych w weryfikacji.
Aktualizacja 22. kwietnia 2014 r .: Tobias Nipkow i Gerwin Klein opublikowali nową książkę
co można uznać za „Winskel in Isabelle / HOL”. Jest to wprowadzenie do semantyki języków programowania (przede wszystkim operacyjnej i aksjomatycznej), ale w przeciwieństwie do wcześniejszych podejść opartych na pisaniu i pisaniu, ta książka wyraża całą swoją matematykę w Isabelle / HOL. Innymi słowy, jest to jednocześnie książka o dowodzeniu twierdzeń.
Książka jest zupełnie nowa, więc nie korzystałem z niej do nauczania, ale wydaje się ona naprawdę odpowiednia jako wstęp, który jest na niższym poziomie niż Software Foundations
autorstwa Pierce i in.