お絵描きベースのカリー／ハワード対応

• 計算科学 -- 型付きラムダ計算とデカルト閉圏
• 論理 -- 自然演繹とシーケント計算

それらを結ぶのが多圏の絵算。どうやって結ぶのか：

1. デカルト閉圏（一般には非対称モノイド閉圏）と厳密多圏の対応を作る。
2. 自然演繹は絵算と同一視する。つまり、自然演繹の証明図＝絵のエンコーディング。
3. 多圏上のシーケント計算を作る。シーケント＝スチル、証明図＝ムービー。
4. 型付きラムダ計算を型シーケント計算の体系にする。
5. 論理のシーケント計算と型シーケント計算を関係づける。