-
- いいね！0
yutakang_jp
@YutakangJ
先週はチャルマール工科大学を訪問しました。来週はインドネシアのバリで開催されるAPLAS2019で、自作のドメイン固有言語LiFtErと数学的帰納法の自動化について話します。conf.researchr.org/home/aplas-2019
2019-11-29 06:01:29
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
APLAS 2019 conf.researchr.org/program/aplas-… NIER pre-workshop1件目、Android JavaとJavaScriptのinteroperation。JavaScriptの静的解析がんばってるグループ、過去研究たくさん。plrg.kaist.ac.kr/doku.php?id=re…
2019-12-01 12:01:19
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
3件目、定数時間保存つきCompCert（形式検証されたCコンパイラ）。暗号ルーチンのタイミングアタック防ぐ目的。
2019-12-01 12:39:13
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
（例えば）GCCのバージョンによっては、ソースレベルでは秘密守っててもコンパイルするとタイミング攻撃で漏洩するおそれ
2019-12-01 12:49:27
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
5件目、path dependent typesの話。popl20.sigplan.org/details/POPL-2… よりauthorが1人多いけど何か違う？
2019-12-01 15:15:33
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
言語としてはScalaとかWyvern wyvernlang.github.io とか。Path dependent typesでgeneritcsとかいろいろ表せるらしい（←雑すぎるまとめ）けどFsub同様、フルセットだと決定不能[Pierce 92]なのでKernel Fsubみたく制限。さらに再帰型もM (material)とS (shape)を区別 cs.cornell.edu/~ross/publicat…
2019-12-01 15:23:37
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
6件目、制約付き文字列の長さに関する問題を解くための、divisibility入りPresburger算術の理論的結果。
2019-12-01 15:45:08
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
7件目。通信パターンの合成等のため、session typeのlabelをfirst-classに。 arxiv.org/abs/1911.00705 wg28.mpi-sws.org/technical-pres… (via wg28.mpi-sws.org/technical-pres…)
2019-12-01 16:43:14
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
8件目、gradual typingで挿入されるcastがtail recursionなどメモリ効率を悪化するので、Hermann他のspace-efficient gradual typingを"coercion-passing style"で実装。Mが値でなくてもM[c][d]→M[c#d]と合成してキャンセル
2019-12-01 17:19:44
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
7件目 twitter.com/esumii/status/… はPOPL 2020にも。popl20.sigplan.org/track/POPL-202…
2019-12-01 17:22:15
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
9件目、ペトリネットやvector addition systemの到達可能性決定問題の計算量解析、最近になって進展(!)、本研究で改善（ザックリ
2019-12-01 17:54:27
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
twitter.com/esumii/status/… "with state"だからVASじゃなくてVASSだった
2019-12-01 18:02:59