第124回プログラミング研究発表会 IPSJPRO 2019-1 実況まとめ

1
Keigo Imai @keigoi

IPSJ-PRO@名古屋の懇親会、申し込みは本日中にお願いします(それ以降でも可能かもしれませんが…)。 6/6(木)18:30- @本山「サロス」 sigpro.ipsj.or.jp/pro2019-1/part… twitter.com/keigoi/status/…

2019-06-02 10:46:38
Keigo Imai @keigoi

#effect_study 宣伝させてください。再来週6/6(木)・7(金)のIPSJ-PRO@名古屋はエフェクト計算の講演2件を初日に予定しています。 twitter.com/keigoi/status/…

2019-05-26 14:41:49
Keigo Imai @keigoi

今日午後からです。名古屋でお待ちしております。 twitter.com/keigoi/status/…

2019-06-06 08:17:08
Keigo Imai @keigoi

プログラミング研究発表会(PRO) 6/6(木)・7(金) @ 名大のプログラムを公開しました:sigpro.ipsj.or.jp/pro2019-1/prog… 初日に今話題のエフェクト計算の講演2件や、2日目にはふくだ @yf0fyf さんの Lisp 実装 github.com/yf-fyf/hlisp の講演もあります!懇親会は6/2(日)までにお申込み!

2019-05-15 08:49:34
Keigo Imai @keigoi

2019-1-(1):14:00-14:30(短い発表) 「ワンショット代数的効果から非対称コルーチンへの変換」 ○河原 悟, 亀山 幸義 (筑波大学) #IPSJPRO sigpro.ipsj.or.jp/pro2019-1/prog…

2019-06-06 14:02:47
Keigo Imai @keigoi

Lua で(ワンショット)代数的効果を実装。ライブラリはこちら!: github.com/Nymphium/eff.l… Multicore OCaml の代数的効果の例を実装して、有用性を確認した twitter.com/keigoi/status/…

2019-06-06 14:18:06
Keigo Imai @keigoi

2019-1-(2):14:30-15:15 「コエフェクト計算に基づく量化型の再形式化」 ○田辺 裕大, Luthfan Anshar Lubis, 青谷 知幸, 増原 英彦 (東京工業大学 大学院情報理工学院 数理・計算科学系) (→ 多相型を線形型システムで表現してみよう!だそう。)

2019-06-06 14:33:30
Keigo Imai @keigoi

型環境中の型変数のスコープの制約のため、線形型システムで可能な型環境の並び替えが多相型システムではできない。同じ枠組みで両方の言語要素を扱いたい → コエフェクト計算 #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 14:40:25
Keigo Imai @keigoi

コエフェクト計算: 線形型システム、アフィン型システムを形式化可能、データフロー言語の型システム、その値の依存ライブラリのバージョン (←著者らの研究) #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 14:42:20
Keigo Imai @keigoi

型システム F⊗ のアイデア:型変数のスコープをその内側の項変数のコエフェクトに対応させる。 #IPSJPRO twitter.com/keigoi/status/… twitter.com/keigoi/status/…

2019-06-06 14:44:32
Keigo Imai @keigoi

Montagu, '18 を参考に型変数に量化の種類(∃,∀)をannotate. 今後やりたいこと:二つの型システム (F⊗ と 線形型) を「混ぜる」.例:module の unpack を2回やってみると型エラーになる.これは線型性と多相型のコエフェクトをそれぞれチェックする.線型性のほうでエラーになる. #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 14:57:44
Keigo Imai @keigoi

Future work: (1) 統合された言語の型安全性のフォーマルな証明。証明の再利用ができそう? (2) 他の型システムとの統合 #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 15:00:20
Keigo Imai @keigoi

質問(塚田さん):型環境の並び替えは System F 程度だと「好みの問題」では。他の (occurrence checkによる) 定式化もある。-> … #IPSJPRO twitter.com/keigoi/status/… twitter.com/keigoi/status/…

2019-06-06 15:06:06
Keigo Imai @keigoi

(スコープの型エラーがどういうコエフェクトの型エラーになるのか見てみたかったね…)

2019-06-06 15:07:03
Keigo Imai @keigoi

2019-1-(3):15:30-16:15 「Solving String Constraints with Streaming String Transducers」 ○朱 啓禎, 赤間 仁志, 南出 靖彦 (東京工業大学情報理工学院数理・計算科学系) #ipsjpro

2019-06-06 15:30:20
Keigo Imai @keigoi

例: let x1=x0.replace("<script>", "x"); let x3=x2.replace("<script>", "x"); let x4 = concat(x1,x3) x0,x2 を任意の文字列とすると x4 は "<script>" を含みうるか?→ Yes (!). こういう問題を扱います #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 15:33:27
Keigo Imai @keigoi

x=T(x) の形の制約は undecidable. Straight-Line に制限するというテクニックが知られている (POPL'16, Lin & Barcelo) #IPSJPRO twitter.com/keigoi/status/…

2019-06-06 15:36:30
Keigo Imai @keigoi

これまでの実装は効率がわるい (SLOTH という実装がある (POPL'18) が文字列のconcatenationを多くのtransductionに置き換え). 本実装は Scala で書かれ,SLOTH より一般に遅いがいくつかのケースで効率がよい.また表現可能な範囲が広い.#IPSJPRO twitter.com/keigoi/status/…

2019-06-06 15:39:02
よんた @keita44_f4

ipsj.ixsq.nii.ac.jp/ej/index.php?a… #IPSJPRO SSTで正規表現をあれこれの話はこの辺かな?ちょうどSSTがよくわからなくて、調べてた。

2019-06-06 15:58:35
Keigo Imai @keigoi

PROの懇親会@本山サロス、飛び入り参加できます!(一名欠員が出たのでぜひ!) 場所は hotpepper.jp/strJ001179921/…

2019-06-06 18:29:54
Keigo Imai @keigoi

今までにないオシャレさ@本山

2019-06-06 18:30:38
よんた @keita44_f4

う、明日も行こうと思ったけど、天気予報で荒れると言っていて、明日の天気が心配になってきた。 #IPSJPRO

2019-06-06 19:36:40
Keigo Imai @keigoi

@mitsu48 またの機会に (明日もやってます)!

2019-06-06 21:38:11
Keigo Imai @keigoi

#IPSJPRO 本日最初は項書き換え系セッション! 2019-1-(4):9:30-10:00(短い発表) 「条件付き項書き換えシステムの十分完全性の自動証明」 ○東和田 直輝, 青戸 等人 (新潟大学大学院 自然科学研究科)

2019-06-07 09:29:13
よんた @keita44_f4

#IPSJPRO signatureは型システムでいいのかな

2019-06-07 09:39:09