セッションタイプ

型理論では、セッション型は並行プログラムの正確性を保証するために使用されます。並行プログラム間で送受信されるメッセージが期待どおりの順序と型であることを保証します。^{[1] [2]セッション型システムは、}チャネルシステムとアクターシステムの両方に適応されています。^[3]

セッションタイプは、同時実行システムや分散システムにおいて望ましい特性、つまり通信エラーやデッドロックがないこと、プロトコルへの準拠を保証するために使用されます。^[4]

2つのプロセス間の相互作用はバイナリセッション型を使用してチェックできますが、3つ以上のプロセス間の相互作用はマルチパーティセッション型を使用してチェックできます。^[5]マルチパーティセッション型では、すべての参加者間の相互作用はグローバル型を使用して記述され、その後、各参加者のローカルビューからの通信を記述するローカル型に投影されます。重要なのは、グローバル型が通信のシーケンス情報をエンコードすることです。これは、同じ通信をバイナリセッション型を使用してエンコードすると失われます。^[6]

バイナリセッションタイプは、送信操作（ ）、受信操作（）、分岐（）、選択（）、再帰（）、終了（ ）を使用して記述できます。^[2]${\displaystyle !}$${\displaystyle ?}$${\displaystyle \&}$${\displaystyle \oplus}$${\displaystyle 記録}$${\displaystyle 終了}$

たとえば、は、最初にブール値( ) を送信し、次に整数( ) を受信して​​、最後に終了する ( )セッション タイプを表します。 ${\displaystyle S=\;!bool.?int.end}$${\displaystyle S}$${\displaystyle !bool}$${\displaystyle ?int}$${\displaystyle 終了}$

セッション タイプは、次のような既存のプログラミング言語に合わせて調整されています。

• lchannels ( Scala ) ^[7]
• エッピ（スカラ）^[7]
• STMonitor（Scala）^[8]
• アンサンブルS ^[9]
• セッションタイプ（Rust）^[10]
• セッシュ（Rust）^[11]
• セッションアクター（Python）^[12]
• 監視セッションErlang ( Erlang ) ^[13]
• FuSe ( OCaml ) ^[14]
• セッション-ocaml (OCaml) ^{[15] [16]}
• 優先度セッシュ（Haskell）^[17]
• Java型状態チェッカー（Java）^{[18] [19] [20]}
• スウィフトセッションズ（スウィフト）^[21]