세션 유형

유형 시스템
일반적인 개념
형식 안전 강한 활자 대 약한 활자
주요 카테고리
스태틱과 다이내믹 매니페스트와 추론 공칭 대 구조 덕 타이핑
마이너 카테고리
추상적인 의존하는 흐름의 영향을 받기 쉽다 서서히 교차로 잠재. 세련 하부 구조 독특한 세션
v t

유형 이론에서 세션 유형은 동시 프로그램에서 정확성을 보장하기 위해 사용됩니다.이를 통해 동시 프로그램 간에 송수신되는 메시지가 예상된 순서와 예상된 ^[1][2]유형의 메시지임을 확인할 수 있습니다.세션 유형 시스템은 채널 ^[3]및 액터 시스템 모두에 대해 조정되었습니다.

세션 유형은 동시 및 분산 시스템에서 바람직한 속성, 즉 통신 오류 및 교착 상태 부재 및 프로토콜 ^[4]준수를 보장하기 위해 사용됩니다.

바이너리 세션유형과 멀티파티 세션유형

2개의 프로세스 간의 상호작용은 바이너리세션 타입을 사용하여 체크할 수 있으며, 3개 이상의 프로세스 간의 상호작용은 멀티 파티세션 ^[5]타입을 사용하여 체크할 수 있습니다.

이진 세션 유형의 정식 정의

바이너리 세션의 유형은 송신 조작$(!\displaystyle!),$ 수신 조작$(?\displaystyle?),$ 브랜치$(\displaystyle\&}),$ 선택$(\displaystyle\oplus}),$ 재귀(${\displaystyle r}$ ${\displaystyle e}$$$$\displaystyle$rec$)$ 및 종료(\$displaystyle$end)$$^[2]를 사용하여 설명할 수 있습니다.

${\displaystyle 예}$를 들어, S${\displaystyle =}$ !${\displaystyle b}$ ${\displaystyle o}$l${\displaystyle }$?${\displaystyle i}$ n${\displaystyle t}$ . ${\displaystyle e}$n d \ $displaystyle$ S = \ ; ! $bool$?int$.end$는 세션타입$$S$(!$ ${\displaystyle b}$ ${\displaystyle \mathrm{ol}}$\ $displaystyle$!$bool$ $$$)$를 나타냅니다$$.그 후 정수${\displaystyle }$ ${\displaystyle \mathrm{in}}$t \ $displaystyle ?int$를 수신한 후 최종적으로 $$합니다( ${\displaystyle \mathrm{en}}$d \ $displaystyle$end$$$$） 。

실장

세션 유형은 다음과 같은 기존 프로그래밍 언어에 맞게 조정되었습니다.

• l채널(Scala)^[6]
• Effpi (스칼라)^[6]
• STMonitor (Scala)^[7]
• 앙상블S^[8].
• 세션 유형(녹)^[9]
• sesh(^[10]녹색)
• 세션 액터(Python)^[11]
• 모니터링 대상 세션 Erlang(Erlang)^[12]
• FuSe(OCAML)^[13]
• session-ocaml(OCAML)^[14][15]
• Priority Sesh(해스켈)^[16]

레퍼런스