長谷川真人さんの "Classical Linear Logic of Implications"https://www.kurims.kyoto-u.ac.jp/~hassei/papers/clli.pdf ：
加法的〈非線形〉コンテキストと乗法的〈線形〉コンテキストを持つ型判断〈typing judgement〉
$`\quad \Gamma ;\Delta \vdash M:\sigma`$
を考える。具体的には、
$`\quad x_1:\sigma_1, \cdots, x_m:\sigma_m ;\, y_1:\tau_1, \cdots,y_n:\sigma_n \vdash M:\sigma`$
これの意味は：
- シーケント $`!\sigma_1, \cdots, !\sigma_m ,\, \tau_1, \cdots, \sigma_n \vdash \sigma`$ の証明が $`M`$ 。
- 命題 $`!\sigma_1 \otimes \cdots \otimes !\sigma_m \otimes \tau_1 \otimes \cdots \otimes \sigma_n \multimap \sigma`$ の証明が $`M`$
二種類の含意を持つが、それは型理論的にアロー型と解釈する。
| 型理論 | 論理 |
|---|---|
| アロー型構成子 | 含意演算 |
| ペア型構成子 | 連言演算 |
| 型 | 命題 |
| 型のインスタンス | 命題の証明〈保証〉 |
| プロファイル | シーケント |
| 型コンテキスト | 平坦バンチ |
| 型判断 | 定理記述 |
| 項 | 証明〈導出〉 |
