Semantyka denotacyjna modelu aktora

Semantyka denotacyjna modelu aktora jest przedmiotem teorii domeny denotacyjnej dla aktorów . Historyczny rozwój tego tematu jest opisany w [Hewitt 2008b].

Semantyka punktu stałego aktora

Denotacyjna teoria semantyki systemów obliczeniowych zajmuje się znajdowaniem obiektów matematycznych, które reprezentują działanie systemów. Zbiory takich obiektów nazywane są domenami . Aktor wykorzystuje domenę scenariuszy diagramów zdarzeń . Zwykle przyjmuje się pewne właściwości domeny, takie jak istnienie granic łańcuchów (patrz cpo ) i element dolny. Różne dodatkowe właściwości są często rozsądne i pomocne: artykuł na temat teorii domen zawiera więcej szczegółów.

Dziedzina jest zwykle porządkiem częściowym , który można rozumieć jako porządek zdefiniowania. Na przykład, biorąc pod uwagę scenariusze diagramu zdarzeń x i y , można by przyjąć, że „ x≤y ” oznacza, że ​​„ y rozszerza obliczenia x ”.

Denotację matematyczną dla systemu S można znaleźć, konstruując coraz lepsze przybliżenia z początkowej pustej denotacji zwanej ⊥ _S przy użyciu denotacji przybliżającej postęp funkcji _S w celu skonstruowania denotacji (znaczenia) dla S w następujący sposób:

$\ Displaystyle \ mathbf {oznaczać} _ {\ mathtt {S}} \ równoważnik \ lim _ {i\to \infty}\mathbf {postęp} _{{\mathtt {S}}^{i}}(\bot _{\mathtt {S}})}$

Należałoby oczekiwać, że progresja _S będzie monotoniczna , tj . jeśli x≤y , to progresja _S (x)≤ progresja _S (y) . Mówiąc bardziej ogólnie, tego byśmy się spodziewali

Jeśli ∀ ja ∈ω x _ja ≤ x _{ja +1} , to ${\ Displaystyle \ mathbf {postęp} _ {\ mathtt {S}} (\ _ {i \ do \ infty}} {\ mathtt {x}} _ {i}) = \ lim _ {i \do \infty}\mathbf {postęp} _{\mathtt {S}}({\mathtt {x}}_{i})}$

Ta ostatnia stwierdzona właściwość progresji _S nazywana jest ciągłością ω.

Centralnym zagadnieniem semantyki denotacyjnej jest scharakteryzowanie, kiedy możliwe jest tworzenie denotacji (znaczenii) zgodnie z równaniem na Denot _S . Podstawowym twierdzeniem teorii dziedzin obliczeniowych jest to, że jeśli postęp _S jest ω-ciągły, to Denot _S będzie istniał.

progresji _S wynika, że

progresja _S ( oznacz _S ) = oznacz _S

Powyższe równanie motywuje terminologię, że Denotacja _S jest stałym punktem _S postępu .

Co więcej, ten stały punkt jest najmniejszy spośród wszystkich stałych punktów progresji _S .

Kompozycjonalność w językach programowania

Ważnym aspektem semantyki denotacyjnej języków programowania jest kompozycyjność, dzięki której denotacja programu jest konstruowana z denotacji jego części. Rozważmy na przykład wyrażenie " <wyrażenie ₁ > + <wyrażenie ₂ > ". Kompozycyjność w tym przypadku polega na nadaniu znaczenia " <wyrażenie ₁ > + <wyrażenie ₂ > " w kategoriach znaczeń <wyrażenie ₁ > i <wyrażenie ₂ > .

Model Actor zapewnia nowoczesny i bardzo ogólny sposób analizy składu programów. Scott i Strachey [1971] zaproponowali, aby semantykę języków programowania sprowadzić do semantyki rachunku lambda iw ten sposób odziedziczyć semantykę denotacyjną rachunku lambda . Okazało się jednak, że obliczeń współbieżnych nie można zaimplementować w rachunku lambda (patrz Nieokreśloność w obliczeniach współbieżnych ). W związku z tym powstał problem, jak zapewnić modułową semantykę denotacyjną dla współbieżnych języków programowania. Jednym z rozwiązań tego problemu jest użycie modelu obliczeniowego Actor. W modelu Actor programy są Aktorami, do których wysyłane są Eval z adresem środowiska (wyjaśnione poniżej), dzięki czemu programy dziedziczą swoją semantykę denotacyjną z semantyki denotacyjnej modelu Actor (pomysł opublikowany w Hewitt [2006]).

Środowiska

Środowiska przechowują powiązania identyfikatorów. Gdy do środowiska zostanie wysłany Lookup z adresem identyfikatora x , zwraca ono najnowsze (leksykalne) powiązanie x .

Jako przykład tego, jak to działa, rozważ poniższe wyrażenie lambda <L> , które implementuje drzewiastą strukturę danych po podaniu parametrów dla leftSubTree i rightSubTree . Kiedy takie drzewo otrzyma komunikat parametru "getLeft" , zwraca leftSubTree i podobnie, gdy otrzyma komunikat "getRight" zwraca rightSubTree .

 λ(leftSubTree, rightSubTree) λ(wiadomość)  if  (message == "getLeft")  then  leftSubTree  else if  (message == "getRight")  then  rightSubTree 

Zastanówmy się, co się stanie, gdy wyrażenie w postaci „(<L> 1 2)” otrzyma wiadomość Eval ze środowiskiem E . Jedna semantyka wyrażeń aplikacji, takich jak ta, jest następująca: <L>, 1 i 2 są wysyłanymi komunikatami Eval ze środowiskiem E . Liczby całkowite 1 i 2 natychmiast odpowiadają sobą na wiadomość Eval .

Jednak <L> odpowiada na wiadomość Eval , tworząc Aktora zamknięcia (proces) C , który ma adres (nazywany body ) dla <L> i adres (nazywany environment ) dla E . Następnie aktor „(<L> 1 2)” wysyła C wiadomość [1 2] .

Kiedy C odbiera komunikat [1 2] , tworzy nowe środowisko Aktor F , który zachowuje się w następujący sposób:

1. Gdy otrzyma wiadomość Lookup dla identyfikatora leftSubTree , odpowiada 1
2. Gdy otrzyma wiadomość Lookup dla identyfikatora rightSubTree , odpowiada 2
3. Po odebraniu komunikatu wyszukiwania dla dowolnego innego identyfikatora przekazuje komunikat wyszukiwania do E

Aktor (proces) C wysyła następnie komunikat Eval ze środowiskiem F do następującego aktora (procesu):

 λ(wiadomość)  if  (wiadomość == "getLeft")  then  leftSubTree  else if  (message == "getRight")  then  rightSubTree 

Wyrażenia arytmetyczne

Jako inny przykład rozważmy aktora dla wyrażenia " <expression ₁ > + <expression ₂ > ", które ma adresy dla dwóch innych aktorów (procesów) <expression ₁ > i <expression ₂ > . Kiedy złożone wyrażenie Aktor (proces) odbiera Eval z adresami dla Aktora środowiska E i klienta C , wysyła komunikaty Eval do <wyrażenia ₁ > i <wyrażenia ₂ > ze środowiskiem E i wysyła C nowego Aktora (proces) C. ₀ _ Gdy C ₀ otrzyma z powrotem dwie wartości N ₁ i N ₂ , wysyła C wartość N ₁ + N ₂ . W ten sposób semantyka denotacyjna dla rachunków procesów i model aktora zapewniają semantykę denotacyjną dla " <wyrażenie ₁ > + <wyrażenie ₂ > " pod względem semantyki dla <wyrażenie ₁ > i <wyrażenie ₂ > .

Inne konstrukcje języka programowania

Przedstawiona powyżej denotacyjna semantyka kompozycyjna jest bardzo ogólna i może być stosowana do programów funkcjonalnych , imperatywnych , współbieżnych , logicznych itp. (zob . [Hewitt 2008a]). Na przykład z łatwością zapewnia semantykę denotacji dla konstrukcji, które są trudne do sformalizowania przy użyciu innych podejść, takich jak opóźnienia i przyszłość .

Model Clingera

W swojej rozprawie doktorskiej Will Clinger opracował pierwszą semantykę denotacji dla modelu aktora.

Dziedzina obliczeń aktora

Clinger [1981] wyjaśnił dziedzinę obliczeń aktora w następujący sposób:

Rozszerzone diagramy zdarzeń aktora [patrz teoria modelu aktora ] tworzą częściowo uporządkowany zestaw < Diagramy , ≤ >, z którego można skonstruować dziedzinę mocy P [ Diagramy ] (patrz sekcja Denotacje poniżej). Rozszerzone diagramy to częściowe historie obliczeń reprezentujące „migawki” [w stosunku do pewnego układu odniesienia] obliczeń w drodze do ukończenia. Dla diagramów x , y ∈ , x≤y oznacza, że ​​x jest etapem, przez który obliczenia mogą przejść w drodze do y . Ukończone elementy Diagramów reprezentują obliczenia, które zakończyły się i obliczenia niekończące się, które stały się nieskończone. Ukończone elementy można abstrakcyjnie scharakteryzować jako maksymalne elementy Diagramów [zob. William Wadge 1979]. Konkretnie, ukończone elementy to te, które mają nieoczekujące zdarzenia. Intuicyjnie Diagramy nie są ω-zupełne , ponieważ istnieją rosnące sekwencje skończonych obliczeń cząstkowych

${\ Displaystyle x_ {0} \ równoważnik x_ {1} \ równoważnik x_ {2} \ równoważnik x_ {3} \ równoważnik ...},$

w którym pewne oczekujące zdarzenie pozostaje w toku na zawsze, podczas gdy liczba zrealizowanych zdarzeń rośnie bez ograniczeń, przeciwnie do wymogu skończonego [przybycia] opóźnienia. Taka sekwencja nie może mieć limitu, ponieważ każdy limit reprezentowałby zakończone niekończące się obliczenie, w którym zdarzenie nadal jest w toku.

Powtórzmy, diagramy diagramów zdarzeń aktora są niekompletne z powodu wymogu skończonego opóźnienia przybycia, co dopuszcza dowolne skończone opóźnienie między zdarzeniem a zdarzeniem, które ono aktywuje, ale wyklucza nieskończone opóźnienie.

denotacje

W swojej rozprawie doktorskiej Will Clinger wyjaśnił, w jaki sposób domeny mocy są uzyskiwane z niekompletnych domen w następujący sposób:

Z artykułu na temat Dziedziny mocy : P [D] to zbiór podzbiorów domeny D domkniętych w dół , które są również domknięte pod istniejącymi najmniejszymi górnymi granicami zbiorów skierowanych w D . Należy zauważyć, że chociaż uporządkowanie na P [D] jest określone przez relację podzbioru, najmniejsze górne granice na ogół nie pokrywają się ze związkami.

Dla domeny diagramów zdarzeń aktora Diagramy element P [ Diagramy ] reprezentuje listę możliwych początkowych historii obliczeń. Ponieważ dla elementów x i y Diagramów x≤y oznacza, że ​​x jest początkowym segmentem początkowej historii y , wymóg, aby elementy P [ Diagramy ] były domknięte w dół, ma wyraźne podstawy w intuicji.

...

Zwykle porządek częściowy, z którego budowana jest dziedzina mocy, musi być ω-zupełny . Są tego dwa powody. Pierwszym powodem jest to, że większość dziedzin potęgowych to po prostu uogólnienia domen, które były używane jako domeny semantyczne w konwencjonalnych programach sekwencyjnych, a wszystkie takie dziedziny są kompletne z powodu konieczności obliczania punktów stałych w przypadku sekwencyjnym. Drugim powodem jest to, że ω-zupełność pozwala na rozwiązanie rekurencyjnych równań dziedziny obejmujących dziedzinę mocy, takich jak

${\ Displaystyle R \ około S \ rightarrow P [S + (S \ razy R)]}$

, która definiuje dziedzinę wznowień [Gordon Plotkin 1976]. Jednak domeny mocy można zdefiniować dla dowolnej domeny. Ponadto dziedzina mocy domeny jest zasadniczo dziedziną mocy jej dopełnienia ω, więc nadal można rozwiązać równania rekurencyjne obejmujące dziedzinę mocy domeny niekompletnej, dostarczając dziedzin, do których zwykłe konstruktory (+, ×, → i *) stosowane są ω-zupełne. Zdarza się, że zdefiniowanie semantyki aktora, jak u Clingera [1981], nie wymaga rozwiązywania żadnych równań rekurencyjnych obejmujących dziedzinę potęgową.

Krótko mówiąc, nie ma technicznych przeszkód w budowaniu domen mocy z niekompletnych domen. Ale dlaczego ktoś miałby chcieć to zrobić?

W semantyce behawioralnej , opracowanej przez Irene Greif , znaczenie programu to specyfikacja obliczeń, które mogą być wykonywane przez program. Obliczenia są formalnie reprezentowane przez diagramy zdarzeń aktora. Greif określił diagramy zdarzeń za pomocą aksjomatów przyczynowych rządzących zachowaniami poszczególnych Aktorów [Greif 1975].

Henry Baker przedstawił niedeterministyczny interpreter generujący chwilowe harmonogramy, które są następnie odwzorowywane na diagramach zdarzeń. Zasugerował, że odpowiedni interpreter deterministyczny działający na zbiorach chwilowych harmonogramów można zdefiniować za pomocą semantyki w dziedzinie potęgowej [Baker 1978].

Semantyka przedstawiona w [Clinger 1981] jest odmianą semantyki behawioralnej. Program oznacza zestaw diagramów zdarzeń Aktora. Zbiór jest definiowany ekstensjonalnie przy użyciu semantyki w dziedzinie potęgi, a nie intencjonalnie przy użyciu aksjomatów przyczynowych. Zachowania poszczególnych Aktorów są zdefiniowane funkcjonalnie. Pokazano jednak, że wynikowy zestaw diagramów zdarzeń Aktora składa się dokładnie z tych diagramów, które spełniają aksjomaty przyczynowe wyrażające zachowania funkcjonalne Aktorów. Zatem semantyka behawioralna Greifa jest kompatybilna z denotacyjną semantyką domeny władzy.

Chwilowe harmonogramy Bakera wprowadziły pojęcie oczekujących zdarzeń , które reprezentują wiadomości w drodze do swoich celów. Każde oczekujące zdarzenie musi prędzej czy później stać się faktycznym (zrealizowanym) zdarzeniem przybycia, co jest wymogiem określanym jako skończone opóźnienie . Rozszerzanie diagramów zdarzeń Aktora o zestawy oczekujących zdarzeń pomaga wyrazić właściwość skończonego opóźnienia, która jest charakterystyczna dla prawdziwej współbieżności [Schwartz 1979].

Obliczenia sekwencyjne tworzą ω-zupełną poddomenę domeny obliczeń aktora

W swojej rozprawie z 1981 roku Clinger pokazał, jak obliczenia sekwencyjne tworzą poddomenę obliczeń współbieżnych:

Zamiast zaczynać od semantyki dla programów sekwencyjnych, a następnie próbować rozszerzyć ją dla współbieżności, semantyka aktora postrzega współbieżność jako podstawową i uzyskuje semantykę programów sekwencyjnych jako przypadek specjalny.

...

Fakt, że istnieją rosnące sekwencje bez najmniejszych górnych granic, może wydawać się dziwny dla tych, którzy są przyzwyczajeni do myślenia o semantyce programów sekwencyjnych. Pomocne może być zwrócenie uwagi, że wszystkie rosnące sekwencje tworzone przez programy sekwencyjne mają najmniejsze górne granice. Rzeczywiście, częściowe obliczenia, które można wykonać za pomocą obliczeń sekwencyjnych, tworzą poddomenę ω-zupełną domeny diagramów obliczeń aktora . Następuje nieformalny dowód.

Z punktu widzenia Aktora, obliczenia sekwencyjne są szczególnym przypadkiem obliczeń współbieżnych, wyróżniających się diagramami zdarzeń. Diagram zdarzeń w obliczeniach sekwencyjnych ma zdarzenie początkowe i żadne zdarzenie nie aktywuje więcej niż jednego zdarzenia. Innymi słowy, kolejność aktywacji obliczeń sekwencyjnych jest liniowa; diagram zdarzeń jest zasadniczo konwencjonalną sekwencją wykonania. Oznacza to, że elementy skończone diagramów

${\ Displaystyle x_ {0} \ równoważnik x_ {1} \ równoważnik x_ {2} \ równoważnik x_ {3} \ równoważnik ...}$

odpowiadające skończonym początkowym segmentom sekwencyjnej sekwencji wykonania wszystkie mają dokładnie jedno oczekujące zdarzenie, z wyjątkiem największy, ukończony element, jeśli obliczenia się zakończą. Jedną z właściwości domeny rozszerzonych diagramów zdarzeń < Diagramy , ≤ > jest to, że jeśli x≤y i x≠y , to pewne oczekujące zdarzenie x jest realizowane w y . Ponieważ w tym przypadku każde x _i ma co najwyżej jedno oczekujące zdarzenie, każde oczekujące zdarzenie w sekwencji zostaje zrealizowane. Stąd ciąg

${\ Displaystyle x_ {0} \ równoważnik x_ {1} \ równoważnik x_ {2} \ równoważnik x_ {3} \ równoważnik ...}$

ma najmniejszą górną granicę na diagramach zgodnie z intuicją.

Powyższy dowód dotyczy wszystkich programów sekwencyjnych, nawet tych z punktami wyboru, takimi jak polecenia strzeżone . Zatem semantyka aktora obejmuje programy sekwencyjne jako przypadek szczególny i zgadza się z konwencjonalną semantyką takich programów.

Model diagramów czasowych

Hewitt [2006b] opublikował nową semantykę denotacyjną dla aktorów opartą na diagramach czasowych. Model diagramów czasowych kontrastuje z modelem Clingera [1981], który skonstruował ω-zupełną dziedzinę mocy z leżącej u jej podstaw niekompletnej dziedziny diagramu, która nie obejmowała czasu. Zaletą modelu dziedzinowego diagramów czasowych jest to, że jest on motywowany fizycznie, a otrzymane obliczenia mają pożądaną właściwość ω-zupełności (a więc nieograniczonego niedeterminizmu), która zapewnia gwarancję usługi.

Dziedzina obliczeń czasowych aktorów

Semantyka denotacyjna diagramów czasowych konstruuje ω-zupełną domenę obliczeniową do obliczeń aktora. W domenie dla każdego zdarzenia w obliczeniach aktora istnieje czas dostarczenia, który reprezentuje czas dostarczenia komunikatu, tak że każdy czas dostarczenia spełnia następujące warunki:

1. Czas dostarczenia to dodatnia liczba wymierna, która nie jest taka sama jak czas dostarczenia jakiejkolwiek innej wiadomości.
2. Czas dostawy jest o więcej niż ustalone δ większy niż czas jego zdarzenia aktywującego. Później okaże się, że wartość δ nie ma znaczenia. W rzeczywistości wartość δ może nawet maleć liniowo w czasie, aby dostosować się do prawa Moore'a.

Diagramy czasowe zdarzeń aktora tworzą częściowo uporządkowany zestaw < TimedDiagrams , ≤>. Diagramy są częściowymi historiami obliczeń reprezentującymi „migawki” (względem pewnego układu odniesienia) obliczeń w drodze do ukończenia. Dla d1, d2ε TimedDiagrams , d1≤d2 oznacza, że ​​d1 jest etapem, przez który obliczenia mogą przejść w drodze do d2. Ukończone elementy TimedDiagrams reprezentują obliczenia, które zakończyły się, i obliczenia niezakończone, które stały się nieskończone. Ukończone elementy można abstrakcyjnie scharakteryzować jako maksymalne elementy TimedDiagrams . Konkretnie, ukończone elementy to te, które nie mają oczekujących zdarzeń.

Twierdzenie: TimedDiagrams jest ω-zupełną dziedziną obliczeń aktora, tj.

1. Jeśli D⊆ TimedDiagrams jest skierowane, istnieje najmniejsza górna granica ⊔D; ponadto ⊔D przestrzega wszystkich praw teorii modelu aktora .
2. Skończone elementy TimedDiagrams są policzalne, gdzie element xε TimedDiagrams jest skończony (izolowany) wtedy i tylko wtedy, gdy D⊆ TimedDiagrams jest skierowany i x≤VD, istnieje dεD z x≤d. Innymi słowy, x jest skończone, jeśli trzeba przejść przez x, aby osiągnąć lub przekroczyć x poprzez proces graniczny.
3. Każdy element TimedDiagrams jest najmniejszą górną granicą policzalnej rosnącej sekwencji elementów skończonych.

Domeny władzy

• Definicja: Dziedzina <Power[ TimedDiagrams] , ⊆> jest zbiorem możliwych początkowych historii M obliczeń takich, że
  1. M jest domknięte w dół, tj. jeśli dεM, to ∀d'εTimedDiagrams d'≤d ⇒ d'εM
  2. M jest domknięte pod najmniejszymi górnymi granicami zbiorów skierowanych, tzn. jeśli D⊆M jest skierowane, to VDεM
• Uwaga: Chociaż Power[ TimedDiagrams ] jest uporządkowany według ⊆, granice nie są określone przez U . tj.

  (∀i∈ω M _i ≤M _i+1 ) ⇒ ​​U _i∈ω M _i ⊆ ⊔ _i∈ω M _i

  Np. If ∀id _i ε Diagramy czasowe i d _i ≤d _i+1 oraz M _i = { d _k | k ≤i} wtedy

  {{{1}}}

• Twierdzenie: Potęga [ TimedDiagrams ] jest dziedziną ω-zupełną.

Twierdzenie o reprezentacji współbieżności

Obliczenia aktora mogą przebiegać na wiele sposobów. Niech d będzie diagramem z następnym zaplanowanym zdarzeniem e i X ≡ {e' | e ─≈→ _{1-wiadomość} e'} (patrz teoria modelu aktora ), Flow(d) jest zdefiniowany jako zbiór wszystkich diagramów czasowych z d i rozszerzeniami d przez X takie, że

1. przybycie wszystkich wydarzeń X zostało zaplanowane gdzie
2. wydarzenia X są zaplanowane we wszystkich możliwych kolejnościach wśród zaplanowanych przyszłych wydarzeń d
3. z zastrzeżeniem, że każde zdarzenie w X jest zaplanowane co najmniej δ po e, a każde zdarzenie w X jest zaplanowane co najmniej raz w każdym następnym przedziale δ.

(Przypomnijmy, że δ to minimalny czas na dostarczenie wiadomości).

Przepływ(d) ≡ {d} jeśli d jest zupełne.

Niech S będzie systemem Aktora, Progresja _S jest odwzorowaniem

Moc [ Diagramy czasowe ]→Moc[ Diagramy czasowe ]

Progresja _S (M) ≡ U _dεM Przepływ(d)

Twierdzenie: Postęp _S jest ω-ciągły.

To znaczy, jeśli ∀i M _i ⊆M _i+1 to Postęp _S (⊔ _iεω M _i ) = ⊔ _iεω Postęp _S (M _i )

Co więcej, najmniej stały punkt Postępu _S jest określony przez twierdzenie o reprezentacji współbieżności w następujący sposób:

⊔ _iεω Progresja _S ⁱ (⊥ _S )

gdzie ⊥ _S jest początkową konfiguracją S.

Denotacja Denot _S systemu aktora S jest zbiorem wszystkich obliczeń S.

Zdefiniuj abstrakcję czasową diagramu czasowego jako diagram z usuniętymi adnotacjami czasowymi.

Twierdzenie o reprezentacji: denotacja denotacji _{S systemu aktora S jest abstrakcją czasu}

⊔ _iεω Progresja _S ⁱ (⊥ _S )

Użycie dziedziny TimedDiagrams , która jest ω-zupełna, jest ważne, ponieważ zapewnia bezpośrednie wyrażenie powyższego twierdzenia o reprezentacji dla denotacji systemów aktorów poprzez bezpośrednie skonstruowanie minimalnego punktu stałego.

Kryterium ciągłości dla wykresów funkcji, którego Scott użył do początkowego opracowania semantyki denotacyjnej funkcji, można wyprowadzić jako konsekwencję praw aktora do obliczeń, jak pokazano w następnej sekcji.

• Dana Scott i Christopher Strachey. W kierunku semantyki matematycznej dla języków komputerowych Monografia techniczna Oxford Programming Research Group. PRG-6. 1971.
• Irena Greif. Semantyka komunikowania się równoległych profesji Rozprawa doktorska MIT EECS. sierpień 1975.
• Joseph E. Stoy , Semantyka denotacyjna: podejście Scotta-Stracheya do semantyki języka programowania . MIT Press , Cambridge, Massachusetts, 1977. (Klasyczny, choć przestarzały podręcznik).
• Gordona Plotkina. Budowa powerdomain SIAM Journal on Computing, wrzesień 1976.
• Edsger Dijkstra . Dyscyplina programowania Prentice Hall . 1976.
• Krzysztof R. Apt , JW de Bakker. Ćwiczenia z semantyki denotacyjnej MFCS 1976: 1-11
• JW de Bakker. Teoria najmniejszych punktów stałych ponownie odwiedzona . Oblicz. nauka 2(2): 155-181 (1976)
• Carl Hewitt i Henry Baker Aktorzy i ciągłe działania funkcjonalne konferencji roboczej IFIP na temat formalnego opisu koncepcji programowania. 1-5 sierpnia 1977.
• Henryk Baker . Systemy aktorów do obliczeń w czasie rzeczywistym Rozprawa doktorska MIT EECS. styczeń 1978.
• Michał Smyth. Domeny mocy Journal of Computer and System Sciences . 1978.
• SAMOCHÓD Hoare . Komunikacja sekwencyjnych procesów CACM . sierpień 1978.
• George'a Milne'a i Robina Milnera . Procesy współbieżne i ich składnia JACM . kwiecień 1979.
• Nissim Francez, CAR Hoare , Daniel Lehmann i Willem-Paul de Roever. Semantyka niedeterminizmu, współbieżności i komunikacji Journal of Computer and System Sciences . grudzień 1979.
• Nancy Lynch i Michaela J. Fischera . O opisywaniu zachowania systemów rozproszonych w semantyce obliczeń współbieżnych. Springer-Verlag . 1979.
• Jerald Schwartz Denotacyjna semantyka równoległości w semantyce obliczeń współbieżnych. Springer-Verlag. 1979.
• Williama Wadge'a. Ekstensjonalne traktowanie zakleszczenia przepływu danych Semantyka współbieżnych obliczeń. Springer-Verlag. 1979.
• Powrót Ralpha-Johana. Semantyka nieograniczonego niedeterminizmu ICALP 1980.
• Dawid Park. O semantyce uczciwego paralelizmu Obrady Szkoły Zimowej w sprawie formalnej specyfikacji oprogramowania. Springer-Verlag. 1980.
• Will Clinger, Podstawy semantyki aktora . MIT Mathematics Doctoral Dissertation, czerwiec 1981. (Cyt. za zgodą autora).
• Carl Hewitt Czym jest zaangażowanie? Fizyczne, organizacyjne i społeczne Pablo Noriega i in. redaktorzy. LNAI 4386. Springer-Verlag. 2007.