Тип сеанса

В теории типов типы сеансов используются для обеспечения корректности в параллельных программах. Они гарантируют, что сообщения, отправляемые и получаемые между параллельными программами, находятся в ожидаемом порядке и ожидаемого типа . ^[1]^[2] Системы сеансового типа были адаптированы как для канальных , так и для актерских систем. ^[3]

Типы сеансов используются для обеспечения желаемых свойств в параллельных и распределенных системах, т. е. отсутствия ошибок связи или взаимоблокировок, а также соответствия протокола. ^[4]

сеансов и многосторонние типы Двоичные

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

Формальное определение типов двоичных сеансов [ править ]

Типы двоичных сеансов можно описать с помощью операций отправки ( $!$ ), получать операции ( $?$ ), филиалы ( $\&$ ), выборки ( $\oplus$ ), рекурсия ( $rec$ ) и прекращение ( $end$ ). ^[2]

Например, $S=\;!bool.?int.end$ представляет тип сеанса $S$ который сначала отправляет логическое значение ( $!bool$ ), затем получает целое число ( $?int$ ) перед окончательным завершением ( $end$ ).

Реализации [ править ]

Типы сеансов были адаптированы для нескольких существующих языков программирования, в том числе:

lканалы ( Скала ) ^[7]
Эффпи (Масштаб) ^[7]
STMonitor (Скала) ^[8]
ансамбли ^[9]
Типы сессий ( Rust ) ^[10]
сеш (Ржавчина) ^[11]
Актеры сеанса ( Python ) ^[12]
Контролируемый сеанс Erlang ( Erlang ) ^[13]
ФуСе ( OCaml ) ^[14]
сеанс-ocaml (OCaml) ^[15]^[16]
Приоритетный Sesh ( Haskell ) ^[17]
Проверка состояния типов Java ( Java ) ^[18]^[19]^[20]

Ссылки [ править ]

^ Хюттель, Ганс; Ланезе, Иван; Васконселос, Васко Т.; Кайрес, Луи; Карбоне, Марко; Дениелу, Пьер-Мало; Мостроус, Димитрис; Падовани, Лука; Равара, Энтони; Туосто, Эмилио; Виейра, Уго Торрес; Заваттаро, Джанлуиджи (5 апреля 2016 г.). «Основы типов сеансов и поведенческих контрактов» . Обзоры вычислительной техники ACM . 49 (1): 3:1–3:36. дои : 10.1145/2873052 . hdl : 2381/38761 . ISSN 0360-0300 . S2CID 3580137 .
^ Jump up to: Перейти обратно: ^а ^б Анкона, Давиде (2016). Поведенческие типы в языках программирования . Ганновер, Массачусетс: Издатели Now. ISBN 978-1-68083-135-1 . OCLC 1053840486 .
^ Фаулер, Саймон; Линдли, Сэм; Вадлер, Филип (10 мая 2017 г.). «Смешивание метафор: актеры как каналы и каналы как актеры (расширенная версия)». arXiv : 1611.06276 [ cs.PL ].
^ Скалас, Альцеста; Ёсида, Нобуко (июнь 2018 г.). «Типы многосторонних сеансов, за пределами двойственности» . Журнал логических и алгебраических методов программирования . 97 : 55–84. дои : 10.1016/j.jlamp.2018.01.001 . hdl : 10044/1/56777 . S2CID 48360420 .
^ Хонда, Кохей; Ёсида, Нобуко; Карбоне, Марко (2008). «Типы многосторонних асинхронных сеансов». Материалы 35-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . стр. 273–284. дои : 10.1145/1328438.1328472 . hdl : 10044/1/26368 . ISBN 9781595936899 . S2CID 53038488 .
^ Ёсида, Нобуко; Гери, Лоренцо (2019). Очень нежное введение в типы многосторонних сеансов . ICDCIT 2020. doi : 10.1007/978-3-030-36987-3_5 .
^ Jump up to: Перейти обратно: ^а ^б «Сессионное программирование на Scala» . alcestes.github.io . Проверено 2 ноября 2021 г.
^ «СТМонитор» . chrisbartoloburlo.github.io . Проверено 2 ноября 2021 г.
^ Харви, Пол; Фаулер, Саймон; Дардха, Орнела; Гей, Саймон Дж. (2021). «Типы многосторонних сеансов для безопасной адаптации среды выполнения на языке актера». 35-я Европейская конференция по объектно-ориентированному программированию (ECOOP 2021) . 194 : 10:1–10:30. doi : 10.4230/LIPIcs.ECOOP.2021.10 . S2CID 234681015 .
^ Йесперсен, Томас Брахт Лауманн; Мунксгаард, Филип; Ларсен, Кен Фриис (30 августа 2015 г.). «Типы сессий для Rust» . Материалы 11-го семинара ACM SIGPLAN по общему программированию . WGP 2015. Ассоциация вычислительной техники. стр. 13–22. дои : 10.1145/2808098.2808100 . ISBN 9781450338103 . S2CID 18320631 .
^ Кокке, Вэнь (12 сентября 2019 г.). «Ржавый вариант: сеансы без тупиков с сбоем в Rust» . Электронные труды по теоретической информатике . 304 : 48–60. arXiv : 1909.05970 . дои : 10.4204/EPTCS.304.4 . ISSN 2075-2180 . S2CID 198166990 .
^ Ёсида, Нобуко; Нейкова, Румяна (29 марта 2017 г.). «Актеры многопартийной сессии» . Логические методы в информатике . 13 (1). дои : 10.23638/LMCS-13(1:17)2017 . S2CID 65240382 .
^ Фаулер, Саймон (10 августа 2016 г.). «Реализация многосторонних участников сеанса на Erlang» . Электронные труды по теоретической информатике . 223 : 36–50. arXiv : 1608.03321 . дои : 10.4204/EPTCS.223.3 . ISSN 2075-2180 . S2CID 418549 .
^ Падовани, Лука (2017). «Простая библиотечная реализация бинарных сессий» . Журнал функционального программирования . 27 :e4. дои : 10.1017/S0956796816000289 . hdl : 2318/1634956 . ISSN 0956-7968 . S2CID 19776781 .
^ Имаи, Кейго; Ёсида, Нобуко; Юэнь, Сёдзи (март 2019 г.). «Session-ocaml: библиотека на основе сеансов с полярностями и линзами» . Наука компьютерного программирования . 172 : 135–159. дои : 10.1016/j.scico.2018.08.005 . hdl : 10044/1/63748 . ISSN 0167-6423 . S2CID 69673075 .
^ Имаи, Кейго. «Сеанс OCaml» . www.ct.info.gifu-u.ac.jp . Проверено 2 ноября 2021 г.
^ Кокке, Вэнь; Дардха, Орнела (26 марта 2021 г.). «Типы сеансов без тупиков в линейном Haskell». arXiv : 2103.14481 [ cs.PL ].
^ «Проверка состояния типов Java» . Гитхаб .
^ Баккиани, Лоренцо; Молодец, Марио; Джунти, Марко; Мота, Жуан; Равара, Антониу (2022). «Проверка состояния типов Java, поддерживающая наследование» . Наука. Программа . 221 : 102844. doi : 10.1016/j.scico.2022.102844 . hdl : 10362/145315 . S2CID 250940803 .
^ Мота, Жуан; Джунти, Марко; Равара, Антониу (2021). «Проверка состояния типов Java» . Материалы КООРДИНАЦИИ 2021 . Конспекты лекций по информатике. Том. 12717. стр. 121–133. дои : 10.1007/978-3-030-78142-2_8 . ISBN 978-3-030-78141-5 . S2CID 235383301 .

Эта по информатике статья незавершена . Вы можете помочь Википедии, расширив ее .

[1] Хюттель, Ганс; Ланезе, Иван; Васконселос, Васко Т.; Кайрес, Луи; Карбоне, Марко; Дениелу, Пьер-Мало; Мостроус, Димитрис; Падовани, Лука; Равара, Энтони; Туосто, Эмилио; Виейра, Уго Торрес; Заваттаро, Джанлуиджи (5 апреля 2016 г.). «Основы типов сеансов и поведенческих контрактов» . Обзоры вычислительной техники ACM . 49 (1): 3:1–3:36. дои : 10.1145/2873052 . hdl : 2381/38761 . ISSN 0360-0300 . S2CID 3580137 .

[behavioraltypes-2] Jump up to: Перейти обратно: ^а ^б Анкона, Давиде (2016). Поведенческие типы в языках программирования . Ганновер, Массачусетс: Издатели Now. ISBN 978-1-68083-135-1 . OCLC 1053840486 .

[3] Фаулер, Саймон; Линдли, Сэм; Вадлер, Филип (10 мая 2017 г.). «Смешивание метафор: актеры как каналы и каналы как актеры (расширенная версия)». arXiv : 1611.06276 [ cs.PL ].

[4] Скалас, Альцеста; Ёсида, Нобуко (июнь 2018 г.). «Типы многосторонних сеансов, за пределами двойственности» . Журнал логических и алгебраических методов программирования . 97 : 55–84. дои : 10.1016/j.jlamp.2018.01.001 . hdl : 10044/1/56777 . S2CID 48360420 .

[5] Хонда, Кохей; Ёсида, Нобуко; Карбоне, Марко (2008). «Типы многосторонних асинхронных сеансов». Материалы 35-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . стр. 273–284. дои : 10.1145/1328438.1328472 . hdl : 10044/1/26368 . ISBN 9781595936899 . S2CID 53038488 .

[6] Ёсида, Нобуко; Гери, Лоренцо (2019). Очень нежное введение в типы многосторонних сеансов . ICDCIT 2020. doi : 10.1007/978-3-030-36987-3_5 .

[alcestes-7] Jump up to: Перейти обратно: ^а ^б «Сессионное программирование на Scala» . alcestes.github.io . Проверено 2 ноября 2021 г.

[8] «СТМонитор» . chrisbartoloburlo.github.io . Проверено 2 ноября 2021 г.

[9] Харви, Пол; Фаулер, Саймон; Дардха, Орнела; Гей, Саймон Дж. (2021). «Типы многосторонних сеансов для безопасной адаптации среды выполнения на языке актера». 35-я Европейская конференция по объектно-ориентированному программированию (ECOOP 2021) . 194 : 10:1–10:30. doi : 10.4230/LIPIcs.ECOOP.2021.10 . S2CID 234681015 .

[10] Йесперсен, Томас Брахт Лауманн; Мунксгаард, Филип; Ларсен, Кен Фриис (30 августа 2015 г.). «Типы сессий для Rust» . Материалы 11-го семинара ACM SIGPLAN по общему программированию . WGP 2015. Ассоциация вычислительной техники. стр. 13–22. дои : 10.1145/2808098.2808100 . ISBN 9781450338103 . S2CID 18320631 .

[11] Кокке, Вэнь (12 сентября 2019 г.). «Ржавый вариант: сеансы без тупиков с сбоем в Rust» . Электронные труды по теоретической информатике . 304 : 48–60. arXiv : 1909.05970 . дои : 10.4204/EPTCS.304.4 . ISSN 2075-2180 . S2CID 198166990 .

[12] Ёсида, Нобуко; Нейкова, Румяна (29 марта 2017 г.). «Актеры многопартийной сессии» . Логические методы в информатике . 13 (1). дои : 10.23638/LMCS-13(1:17)2017 . S2CID 65240382 .

[13] Фаулер, Саймон (10 августа 2016 г.). «Реализация многосторонних участников сеанса на Erlang» . Электронные труды по теоретической информатике . 223 : 36–50. arXiv : 1608.03321 . дои : 10.4204/EPTCS.223.3 . ISSN 2075-2180 . S2CID 418549 .

[14] Падовани, Лука (2017). «Простая библиотечная реализация бинарных сессий» . Журнал функционального программирования . 27 :e4. дои : 10.1017/S0956796816000289 . hdl : 2318/1634956 . ISSN 0956-7968 . S2CID 19776781 .

[15] Имаи, Кейго; Ёсида, Нобуко; Юэнь, Сёдзи (март 2019 г.). «Session-ocaml: библиотека на основе сеансов с полярностями и линзами» . Наука компьютерного программирования . 172 : 135–159. дои : 10.1016/j.scico.2018.08.005 . hdl : 10044/1/63748 . ISSN 0167-6423 . S2CID 69673075 .

[16] Имаи, Кейго. «Сеанс OCaml» . www.ct.info.gifu-u.ac.jp . Проверено 2 ноября 2021 г.

[17] Кокке, Вэнь; Дардха, Орнела (26 марта 2021 г.). «Типы сеансов без тупиков в линейном Haskell». arXiv : 2103.14481 [ cs.PL ].

[18] «Проверка состояния типов Java» . Гитхаб .

[19] Баккиани, Лоренцо; Молодец, Марио; Джунти, Марко; Мота, Жуан; Равара, Антониу (2022). «Проверка состояния типов Java, поддерживающая наследование» . Наука. Программа . 221 : 102844. doi : 10.1016/j.scico.2022.102844 . hdl : 10362/145315 . S2CID 250940803 .

[20] Мота, Жуан; Джунти, Марко; Равара, Антониу (2021). «Проверка состояния типов Java» . Материалы КООРДИНАЦИИ 2021 . Конспекты лекций по информатике. Том. 12717. стр. 121–133. дои : 10.1007/978-3-030-78142-2_8 . ISBN 978-3-030-78141-5 . S2CID 235383301 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]