Денотационная семантика

Изучение языков программирования через математические объекты

В информатике денотатационная семантика (первоначально известная как математическая семантика или семантика Скотта-Стрейчи ) — это подход к формализации значений языков программирования путем построения математических объектов (называемых денотациями ), которые описывают значения выражений из языков. Другие подходы, обеспечивающие формальную семантику языков программирования, включают аксиоматическую семантику и операционную семантику .

В широком смысле денотационная семантика занимается поиском математических объектов, называемых доменами , которые представляют то, что делают программы. Например, программы (или программные фразы) могут быть представлены частичными функциями ^{[1] [2]} или играми ^[3] между средой и системой.

Важным принципом денотационной семантики является то, что семантика должна быть композиционной : денотат программной фразы должен строиться из денотатов ее подфраз .

Историческое развитие

Денотационная семантика возникла в работах Кристофера Стрейчи и Даны Скотт , опубликованных в начале 1970-х годов. ^{[1] [2]} Первоначально разработанная Стрейчи и Скоттом, денотатационная семантика определяла значение компьютерной программы как функции , которая отображает входные данные в выходные данные. ^[2] Чтобы придать смысл рекурсивно определенным программам, Скотт предложил работать с непрерывными функциями между областями , в частности с полными частичными порядками . Как описано ниже, продолжалась работа по исследованию подходящей денотационной семантики для таких аспектов языков программирования, как последовательность, параллелизм, недетерминизм и локальное состояние .

Денотационная семантика была разработана для современных языков программирования, которые используют такие возможности, как параллелизм и исключения , например, Concurrent ML , ^[4] CSP , ^[5] и Haskell . ^[6] Семантика этих языков композиционная, поскольку значение фразы зависит от значений ее подфраз. Например, значение аппликативного выражения f(E1,E2) определяется с точки зрения семантики его подфраз f, E1 и E2. В современном языке программирования E1 и E2 могут оцениваться одновременно, и выполнение одного из них может повлиять на другой, взаимодействуя через общие объекты , в результате чего их значения будут определяться друг с другом. Кроме того, E1 или E2 могут вызвать исключение, которое может прервать выполнение другого. В разделах ниже описываются особые случаи семантики этих современных языков программирования.

Значения рекурсивных программ

Денотационная семантика приписывается программной фразе как функция от среды (содержащей текущие значения ее свободных переменных) до ее обозначения. Например, фраза n*mсоздает обозначение, если ей предоставляется среда, в которой есть привязка для двух ее свободных переменных: nи m. Если в среде nимеет значение 3 и mимеет значение 5, то обозначение равно 15. ^[2]

Функцию можно представить как набор упорядоченных пар аргументов и соответствующих значений результатов. Например, набор {(0,1), (4,3)} обозначает функцию с результатом 1 для аргумента 0, результатом 3 для аргумента 4 и неопределенным в противном случае.

Рассмотрим, например , функцию факториала , которую можно рекурсивно определить как:

int факториал ( int n ) { if ( n == 0 ) то вернуть 1 ; иначе вернуть n * факториал ( n -1 ); }                

Чтобы придать смысл этому рекурсивному определению, обозначение построено как предел приближений, где каждое приближение ограничивает количество вызовов факториала. Вначале мы начинаем без вызовов — следовательно, ничего не определено. В следующем приближении мы можем добавить упорядоченную пару (0,1), поскольку для этого не требуется повторно вызывать факториал. Аналогичным образом мы можем добавить (1,1), (2,2) и т. д., добавляя по одной паре в каждом последовательном приближении, поскольку для вычисления факториала (n) требуется n+1 вызовов. В пределе мы получаем полную функцию от до, определенную всюду в своей области определения. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

Формально мы моделируем каждое приближение как частичную функцию . Наше приближение затем многократно применяет функцию, реализующую «сделать более определенную частичную функцию факториала», т. е. начиная с пустой функции (пустого множества). F можно определить в коде следующим образом (используя for ): ${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$ ${\displaystyle F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )}$Map<int,int> ${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$

intfactorial_nonrecursive ( Map < int , int > factorial_less_defined , int n ) { if ( n == 0 ) then return 1 ;​ иначе if ( fprev = поиск ( factorial_less_defined , n -1 )) тогда верните n * fprev ; иначе верните NOT_DEFINED ; }                         Map < int , int > F ( Map < int , int > factorial_less_defined ) { Map < int , int > new_factorial = Map . пустой (); for ( int n in all < int > ()) { if ( f = Factorial_nonrecursive ( factorial_less_define , n ) != NOT_DEFINED ) new_factorial . положить ( н , ж ); } Вернуть новый_факториал ; }                         

Затем мы можем ввести обозначение Fn ^, чтобы указать, что F применяется n раз .

• F ⁰ ({}) — полностью неопределенная частичная функция, представленная как множество {};
• F ¹ ({}) — частичная функция, представленная как набор {(0,1)}: она определена в 0, равна 1 и не определена в другом месте;
• F ⁵ ({}) — частичная функция, представленная в виде множества {(0,1), (1,1), (2,2), (3,6), (4,24)}: она определена для аргументы 0,1,2,3,4.

Этот итерационный процесс строит последовательность частичных функций от до . Частичные функции образуют полный по цепочке частичный порядок, используя ⊆ в качестве порядка. Более того, этот итерационный процесс лучших приближений факториальной функции образует расширяющее (также называемое прогрессивным) отображение, поскольку каждое из них использует ⊆ в качестве порядка. Таким образом, согласно теореме о неподвижной точке (в частности, теореме Бурбаки–Витта ) для этого итерационного процесса существует неподвижная точка. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle F^{i}\leq F^{i+1}}$

В данном случае неподвижной точкой является наименьшая верхняя граница этой цепочки, представляющая собой полную factorialфункцию, которую можно выразить как объединение

${\displaystyle \bigcup _{i\in \mathbb {N} }F^{i}(\{\}).}$

Найденная нами фиксированная точка является наименее фиксированной точкой F , поскольку наша итерация началась с наименьшего элемента в области определения (пустого набора). Чтобы доказать это, нам понадобится более сложная теорема о неподвижной точке, такая как теорема Кнастера – Тарского .

Денотационная семантика недетерминированных программ

Концепция доменов мощности была разработана для придания денотационной семантики недетерминированным последовательным программам. Записывая P для конструктора степенной области, область P ( D ) является областью недетерминированных вычислений типа, обозначенного D .

Существуют трудности со справедливостью и неограниченностью в теоретико-предметных моделях недетерминизма. ^[7]

Денотационная семантика параллелизма

Многие исследователи утверждают, что теоретико-предметные модели, приведенные выше, недостаточны для более общего случая параллельных вычислений . По этой причине были представлены различные новые модели . В начале 1980-х годов люди начали использовать стиль денотационной семантики для определения семантики параллельных языков. Примеры включают работу Уилла Клингера с моделью актера ; работа Глинна Винскеля со структурами событий и сетями Петри ; ^[8] и работу Франсеса, Хоара, Лемана и де Ровера (1979) по семантике трассировки для CSP. ^[9] Все эти направления исследований остаются в стадии исследования (см., например, различные денотационные модели для CSP ^[5] ).

Недавно Винскель и другие предложили категорию профункторов в качестве теории предметной области параллелизма. ^{[10] [11]}

Денотационная семантика состояния

Состояние (например, куча) и простые императивные функции можно напрямую смоделировать с помощью денотационной семантики, описанной выше. Основная идея состоит в том, чтобы рассматривать команду как частичную функцию в некоторой области состояний. Значение " x:=3" - это функция, которая переводит состояние в состояние с 3присвоенным значением x. Оператор последовательности " ;" обозначается композицией функций. Затем конструкции с фиксированной точкой используются для придания семантики циклическим конструкциям, таким как " while".

Все становится сложнее при моделировании программ с локальными переменными. Один из подходов состоит в том, чтобы больше не работать с доменами, а вместо этого интерпретировать типы как функторы из некоторой категории миров в категорию доменов. Программы тогда обозначаются естественными непрерывными функциями между этими функторами. ^{[12] [13]}

Обозначения типов данных

Многие языки программирования позволяют пользователям определять рекурсивные типы данных . Например, тип списков номеров можно указать с помощью

 список  типов данных =  Минусы  nat  *  list |  Пустой  

В этом разделе рассматриваются только функциональные структуры данных, которые не могут быть изменены. Обычные императивные языки программирования обычно позволяют изменять элементы такого рекурсивного списка.

Другой пример: тип обозначений нетипизированного лямбда -исчисления:

тип данных  D  =  D  из  ( D  →  D )

Проблема решения уравнений предметной области связана с поиском областей, моделирующих такие типы данных. Грубо говоря, один из подходов состоит в том, чтобы рассматривать совокупность всех доменов как сам домен, а затем решать там рекурсивное определение.

Полиморфные типы данных — это типы данных, определенные с помощью параметра. Например, тип α lists определяется выражением

 тип данных α  список  =  Минусы  α  * α  список | Пустой    

Таким образом, списки натуральных чисел имеют тип nat list, а списки строк — тип string list.

Некоторые исследователи разработали теоретико-доменные модели полиморфизма. Другие исследователи также моделировали параметрический полиморфизм в рамках конструктивных теорий множеств.

Недавняя область исследований связана с денотационной семантикой для языков программирования, основанных на объектах и ​​классах. ^[14]

Денотатационная семантика для программ ограниченной сложности.

После развития языков программирования, основанных на линейной логике , денотационная семантика была передана языкам для линейного использования (см., например, сети доказательств , пространства когерентности ), а также полиномиальную временную сложность. ^[15]

Денотационная семантика последовательности

Проблема полной абстракции для языка последовательного программирования PCF долгое время была большим открытым вопросом в денотационной семантике. Трудность с PCF заключается в том, что это очень последовательный язык. Например, в PCF невозможно определить функцию « параллельное-или» . Именно по этой причине подход с использованием доменов, представленный выше, дает денотационную семантику, которая не является полностью абстрактной.

Этот открытый вопрос был в основном решен в 1990-х годах с развитием семантики игр , а также с помощью методов, включающих логические отношения . ^[16] Более подробную информацию см. на странице PCF.

Денотационная семантика как перевод из источника в источник

Часто бывает полезно перевести один язык программирования на другой. Например, язык параллельного программирования может быть переведен в исчисление процессов ; язык программирования высокого уровня может быть переведен в байт-код. (Действительно, традиционную денотационную семантику можно рассматривать как интерпретацию языков программирования во внутренний язык категории предметных областей.)

В этом контексте понятия денотационной семантики, такие как полная абстракция, помогают удовлетворить проблемы безопасности. ^{[17] [18]}

Абстракция

Часто считается важным связать денотационную семантику с операционной семантикой . Это особенно важно, когда денотационная семантика скорее математическая и абстрактная, а операционная семантика более конкретна или близка к вычислительной интуиции. Часто представляют интерес следующие свойства денотационной семантики.

1. Синтаксическая независимость : обозначения программ не должны включать синтаксис исходного языка.
2. Адекватность (или надежность) : Все наблюдаемые различные программы имеют разные значения;
3. Полная абстракция : все программы, эквивалентные наблюдениям, имеют одинаковые обозначения.

Для семантики в традиционном стиле адекватность и полную абстракцию можно понимать примерно как требование, чтобы «операционная эквивалентность совпадала с денотационным равенством». Для денотационной семантики в более интенсиональных моделях, таких как модель актера и исчисление процессов , внутри каждой модели существуют разные понятия эквивалентности, поэтому концепции адекватности и полной абстракции являются предметом споров, и их труднее определить. Также математическая структура операционной семантики и денотационной семантики может стать очень близкой.

Дополнительные желательные свойства, которые мы можем захотеть сохранить между операционной и денотационной семантикой:

1. Конструктивизм : Конструктивизм касается того, можно ли доказать существование элементов предметной области конструктивными методами.
2. Независимость денотационной и операционной семантики . Денотационная семантика должна быть формализована с использованием математических структур, независимых от операционной семантики языка программирования; Однако лежащие в основе концепции могут быть тесно связаны. См. раздел «Композиционность» ниже.
3. Полная полнота или определимость : каждый морфизм семантической модели должен быть обозначением программы. ^[19]

Композиционность

Важным аспектом денотационной семантики языков программирования является композиционность, при которой денотат программы строится из обозначений ее частей. Например, рассмотрим выражение «7+4». Композиционность в данном случае заключается в том, чтобы обеспечить значение «7 + 4» с точки зрения значений «7», «4» и «+».

Основная денотационная семантика в теории предметной области является композиционной, поскольку она задается следующим образом. Начнем с рассмотрения фрагментов программ, т.е. программ со свободными переменными. Контекст типизации присваивает тип каждой свободной переменной. Например, выражение ( x + y ) может рассматриваться в контексте типизации ( x : nat, y : nat). Теперь придадим денотационную семантику фрагментам программы, используя следующую схему.

1. Начнем с описания значения типов нашего языка: значение каждого типа должно быть областью. Обозначим 〚τ〛 область, обозначающую тип τ. Например, значение типа natдолжно быть областью натуральных чисел: 〚nat〛= _⊥ . ${\displaystyle \mathbb {N} }$
2. Из значения типов мы получаем значение контекстов типизации. Положим 〚x ₁ :τ ₁ ,..., x _n :τ _n〛 = 〚 τ ₁〛× ... ×〚τ _n〛. Например, 〚x : nat, y : nat〛= _⊥ × _⊥ . В частном случае значение пустого контекста типизации без переменных — это домен с одним элементом, обозначаемым 1. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$
3. Наконец, мы должны придать смысл каждому фрагменту программы в контексте типизации. Предположим, что P — это фрагмент программы типа σ, в контексте типизации Γ, часто записываемый Γ⊢ P :σ. Тогда смысл этой программы в контексте типизации должен быть непрерывной функцией 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛. Например, 〚⊢7: nat〛:1→ _⊥ — это функция, постоянно имеющая число «7», а 〚x : , y : ⊢ x + y : 〛: _⊥ × _⊥ → _⊥ — функция, которая складывает два числа. ${\displaystyle \mathbb {N} }$natnatnat ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

Теперь смысл составного выражения (7+4) определяется путем составления трех функций 〚⊢7: nat〛:1→ _⊥ , 〚⊢4: 〛:1→ _⊥ и 〚x : , y : ⊢ x + y : 〛: _⊥ × _⊥ → _⊥ . ${\displaystyle \mathbb {N} }$nat ${\displaystyle \mathbb {N} }$natnatnat ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

По сути, это общая схема композиционной денотационной семантики. Здесь нет ничего конкретного о доменах и непрерывных функциях. Вместо этого можно работать с другой категорией . Например, в семантике игр категория игр включает игры как объекты и стратегии как морфизмы: мы можем интерпретировать типы как игры, а программы как стратегии. Для простого языка без общей рекурсии мы можем обойтись категорией множеств и функций . Для языка с побочными эффектами мы можем работать с монадой в категории Клейсли . Для языка с состоянием мы можем работать в категории функторов . Милнер выступал за моделирование местоположения и взаимодействия, работая в категории, где интерфейсы являются объектами, а биграфы — морфизмами. ^[20]

Семантика против реализации

По словам Даны Скотт (1980): ^[21]

Семантика не обязательно определяет реализацию, но она должна предоставлять критерии, показывающие, что реализация правильна.

По данным Клингера (1981): ^{[22] : 79.}

Однако обычно формальная семантика обычного языка последовательного программирования сама по себе может интерпретироваться как (неэффективная) реализация языка. Однако формальная семантика не всегда должна обеспечивать такую ​​реализацию, и мнение, что семантика должна обеспечивать реализацию, приводит к путанице в отношении формальной семантики параллельных языков. Такая путаница становится до боли очевидной, когда говорят, что наличие неограниченного недетерминизма в семантике языка программирования подразумевает, что этот язык программирования не может быть реализован.

Связи с другими областями информатики

В некоторых работах по денотационной семантике типы интерпретируются как области в смысле теории доменов, которую можно рассматривать как ветвь теории моделей , что приводит к связям с теорией типов и теорией категорий . В информатике существуют связи с абстрактной интерпретацией , проверкой программ и проверкой моделей .

Рекомендации

1. Дана С. Скотт. Очерк математической теории вычислений. Техническая монография PRG-2, Вычислительная лаборатория Оксфордского университета, Оксфорд, Англия, ноябрь 1970 г.
2. Дана Скотт и Кристофер Стрейчи . К математической семантике компьютерных языков. Техническая монография Оксфордской исследовательской группы по программированию. ПРГ-6. 1971.
3. Ян Юрьенс. J. Игры в семантике языков программирования – элементарное введение. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034
4. Джон Реппи «Параллельное машинное обучение: проектирование, применение и семантика» в Springer-Verlag, Конспекты лекций по информатике , Vol. 693. 1993 г.
5. AW Роско . «Теория и практика параллелизма» Прентис-Холл. Пересмотрено в 2005 году.
6. Саймон Пейтон Джонс , Аластер Рид, Фергюс Хендерсон, Тони Хоар и Саймон Марлоу. Конференция «Семантика неточных исключений» по проектированию и реализации языков программирования. 1999.
7. Леви, Пол Блейн (2007). «Amb нарушает благоразумие, а Ground Amb - нет». Электрон. Примечания Теор. Вычислить. Наука . 173 : 221–239. дои : 10.1016/j.entcs.2007.02.036 .
8. Семантика структуры событий для CCS и родственных языков . Отчет об исследовании DAIMI, Орхусский университет, 67 стр., апрель 1983 г.
9. Ниссим Франсез , КАР Хоар , Дэниел Леманн и Виллем-Поль де Ровер. «Семантика недетерминизма, параллелизма и коммуникации», Журнал компьютерных и системных наук . Декабрь 1979 года.
10. Каттани, Джан Лука; Винскель, Глинн (2005). «Профункторы, открытые карты и бисимуляция». Математические структуры в информатике . 15 (3): 553–614. CiteSeerX 10.1.1.111.6243 . дои : 10.1017/S0960129505004718. S2CID  16356708. 
11. Найгаард, Миккель; Винскель, Глинн (2004). «Теория предметной области для параллелизма». Теор. Вычислить. Наука . 316 (1–3): 153–190. дои : 10.1016/j.tcs.2004.01.029 .
12. Питер В. О'Хирн , Джон Пауэр, Роберт Д. Теннент, Макото Такэяма. Еще раз о синтаксическом контроле интерференции. Электрон. Примечания Теор. Вычислить. наук. 1. 1995.
13. Фрэнк Дж. Олес. Теоретико-категорный подход к семантике программирования . Докторская диссертация, Сиракузский университет , Нью-Йорк, США. 1982.
14. Реус, Бернхард; Штрайхер, Томас (2004). «Семантика и логика объектных исчислений». Теор. Вычислить. Наука . 316 (1): 191–213. дои : 10.1016/j.tcs.2004.01.030 .
15. Байо, П. (2004). «Стратифицированные когерентные пространства: денотатационная семантика легкой линейной логики». Теор. Вычислить. Наука . 318 (1–2): 29–55. дои : 10.1016/j.tcs.2003.10.015 .
16. О'Хирн, PW; Рике, JG (июль 1995 г.). «Логические отношения Крипке и ПКФ». Информация и вычисления . 120 (1): 107–116. дои : 10.1006/inco.1995.1103 . S2CID  6886529.
17. Мартин Абади. «Защита при переводах с языков программирования». Учеб. ICALP'98 . ЛНКС 1443. 1998.
18. Кеннеди, Эндрю (2006). «Защита модели программирования .NET». Теор. Вычислить. Наука . 364 (3): 311–7. дои : 10.1016/j.tcs.2006.08.014 .
19. Курьен, Пьер-Луи (2007). «Определимость и полная абстракция». Электронные заметки по теоретической информатике . 172 : 301–310. дои : 10.1016/j.entcs.2007.02.011 .
20. Милнер, Робин (2009). Пространство и движение общающихся агентов . Издательство Кембриджского университета. ISBN 978-0-521-73833-0.Черновик 2009 г. Архивировано 2 апреля 2012 г. в Wayback Machine .
21. «Что такое денотационная семантика?», Серия выдающихся лекций Лаборатории компьютерных наук Массачусетского технологического института, 17 апреля 1980 г., цитируется в Clinger (1981).
22. Клингер, Уильям Д. (май 1981 г.). Основы акторной семантики (кандидатская диссертация). Массачусетский Институт Технологий. hdl : 1721.1/6935 . АИТР-633.

дальнейшее чтение

Учебники

• Милн, РЭ; Стрейчи, К. (1976). Теория семантики языков программирования . ISBN 978-1-5041-2833-9.
• Гордон, MJC (2012) [1979]. Денотационное описание языков программирования: введение. Спрингер. ISBN 978-1-4612-6228-2.
• Стой, Джозеф Э. (1977). Денотационная семантика: подход Скотта-Стрейчи к семантике языка программирования . МТИ Пресс. ISBN 978-0-262-19147-0.(Классический, хотя и устаревший учебник.)
• Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . Аллин и Бэкон. ISBN 978-0-205-10450-5.
  • сейчас распродан; доступна бесплатная электронная версия: Шмидт, Дэвид А. (1997) [1986]. Денотационная семантика: методология развития языка. Канзасский государственный университет.
• Гюнтер, Карл (1992). Семантика языков программирования: структуры и методы . МТИ Пресс. ISBN 978-0-262-07143-7.
• Винскель, Глинн (1993). Формальная семантика языков программирования . МТИ Пресс. ISBN 978-0-262-73103-4.
• Теннент, Р.Д. (1994). «Денотативная семантика». В Абрамский С.; Габбай, Дов М.; Майбаум, TSE (ред.). Семантические структуры . Справочник по логике в информатике. Том. 3. Издательство Оксфордского университета. стр. 169–322. ISBN 978-0-19-853762-5.
• Абрамский, С. ; Юнг, А. (1994). «Теория предметной области» (PDF) . Абрамский, Габбай и Майбаум 1994 .
• Столтенберг-Хансен, В.; Линдстрем, И.; Гриффор, ER (1994). Математическая теория областей . Издательство Кембриджского университета. ISBN 978-0-521-38344-8.

Конспект лекций

• Винскель, Глинн. «Денотационная семантика» (PDF) . Кембриджский университет.

Другие ссылки

• Грейф, Ирен (август 1975 г.). Семантика взаимодействия параллельных процессов (PDF) (кандидатская диссертация). Проект МАК. Массачусетский Институт Технологий. АДА016302.
• Плоткин, Г.Д. (1976). «Конструкция области власти». СИАМ Дж. Компьютер . 5 (3): 452–487. CiteSeerX  10.1.1.158.4318 . дои : 10.1137/0205035.
• Дейкстра, Эдсгер В. (1976). Дисциплина программирования . Ряд Прентиса-Холла в автоматических вычислениях. Энглвуд Клиффс, ISBN Нью-Джерси 0-13-215871-Х. ОСЛК  1958445.{{cite book}}: CS1 maint: location missing publisher (link)
• Апт, Кшиштоф Р .; де Баккер, JW (1976). Упражнения по денотационной семантике . Афделинг Информатика. Амстердам: Математический центр. ОСЛК  63400684.
• Де Баккер, JW (1976). «Возвращение к наименее фиксированным точкам». Теоретическая информатика . 2 (2): 155–181. дои : 10.1016/0304-3975(76)90031-1 .
• Смит, Майкл Б. (1978). «Домены власти». Дж. Компьютер. Сист. Наука . 16 :23–36. дои : 10.1016/0022-0000(78)90048-X .
• Франсез, Ниссим; Хоар, ЦАР; Леманн, Дэниел; де Ровер, Виллем-Поль (декабрь 1979 г.). Семантика недетерминизма, параллелизма и коммуникации . Конспекты лекций по информатике. Том. 64. стр. 191–200. дои : 10.1007/3-540-08921-7_67. hdl : 1874/15886. ISBN 978-3-540-08921-6. {{cite book}}: |work=игнорируется ( помощь )
• Линч, Нэнси ; Фишер, Майкл Дж. (1979). «Об описании поведения распределенных систем». Ин Кан, Г. (ред.). Семантика параллельных вычислений: материалы международного симпозиума, Эвиан, Франция, 2-4 июля 1979 г. Спрингер. ISBN 978-3-540-09511-8.
• Шварц, Джеральд (1979). «Денотационная семантика параллелизма». Кан 1979 .
• Уодж, Уильям (1979). «Расширенное лечение тупиковой ситуации потока данных». Кан 1979 .
• Назад, Ральф-Йохан (1980). «Семантика неограниченного недетерминизма». Ин де Баккер, Жако; ван Леувен, Ян (ред.). Автоматы, языки и программирование. Конспекты лекций по информатике. Том. 85. Берлин, Гейдельберг: Шпрингер. стр. 51–63. дои : 10.1007/3-540-10003-2_59. ISBN 978-3-540-39346-7. ОСЛК  476017025.
• Парк, Дэвид (1980). «О семантике справедливого параллелизма». В Бьёрнере, Дайнс (ред.). Абстрактные спецификации программного обеспечения (PDF) . Конспекты лекций по информатике. Том. 86. Берлин, Гейдельберг: Springer Berlin Heidelberg. стр. 504–526. дои : 10.1007/3-540-10007-5_47. ISBN 978-3-540-10007-2.
• Эллисон, Л. (1986). Практическое введение в денотационную семантику. Издательство Кембриджского университета. ISBN 978-0-521-31423-7.
• Америка, П.; де Баккер, Дж.; Кок, Дж. Н.; Руттен, Дж. (1989). «Денотационная семантика параллельного объектно-ориентированного языка». Информация и вычисления . 83 (2): 152–205. дои : 10.1016/0890-5401(89)90057-6 . S2CID  2405175.
• Шмидт, Дэвид А. (1994). Структура типизированных языков программирования . МТИ Пресс. ISBN 978-0-262-69171-0.

Внешние ссылки

• Денотационная семантика. Обзор книги Ллойда Эллисона
• Шрайнер, Вольфганг (1995). «Структура языков программирования I: денотационная семантика». Примечания к курсу .