Formalna semantyka języków programowania

Jestem nowy w teorii języków programowania i szukam dobrego zasobu na temat zasobów dla formalnej semantyki języków programowania. Poszukuje strukturalnej semantyki operacyjnej. Mam rekomendacje książek. Ale szukam zasobu na bardziej wstępnym poziomie. Mile widziane są zwłaszcza samouczki, strona internetowa i bezpłatne rekomendacje książek.

Patrząc na kurs semantyki operacyjnej na moim uniwersytecie, otrzymuję następujące trzy:

• Notatki z wykładu Andrew Pittsa
• Notatki Aarhus Gordona Plotkina na temat strukturalnej semantyki operacyjnej
• Semantyka języków programowania Matthew Hennessey

Ohad.

Semantyka strukturalna operacyjna (SOS) jest bardzo ogólną koncepcją. Zasadniczo jest to relacja binarna w konfiguracjach (zwykle programy plus kontekst, taki jak stan lub dostępne kontynuacje), lub, w przypadku semantyki oznaczonej, relacja trójskładnikowa między konfiguracjami, działaniami (które reprezentują pewne minimalne konteksty) i konfiguracjami. „Strukturalny” bit polega zwykle na tym, że relacje te są definiowane indukcyjnie w ramach zaangażowanej składni (np. Konfiguracje i akcje).

Jako takie, bez innych wymagań, jednostki matematyczne, które rozważamy w SOS, są zbyt ogólne, aby same w sobie były interesujące / możliwe do przełożenia.

SOS staje się interesujący i istotny, gdy spojrzymy na specjalne przypadki, np. Równoważności dla rachunku czasowego, oznakowane przejścia dla asynchronicznego rachunku otoczenia odpowiadające redukcjom lub pytania o ekspresyjność niektórych (klas) rachunku.

Tak więc moim zaleceniem dla pana / pani Systemfault jest pominięcie ogólników i przejście od razu do konkretnego rachunku zainteresowania. Po drodze można łatwo podnieść ogólne techniki SOS.

Poleciłbym przeczytać rozdział 2 w tej książce do pobrania:

Semantyka z aplikacjami: formalne wprowadzenie, Hanne Riis Nielson i Flemming Nielson, Wiley, 1992. http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html