https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #etaps2014 https://t.co/KgfXU8XrNA の研究の話を聞いている。研究の方の話は後で書くとして、TouchDevelop知らなかったんだけど良さげですね。変に特化してない割と普通のプログラムも書けるタッチ用言語/環境、自分で作ろうかと思ってたとこだった | |
| 具体的には競技プログラミングの問題を出先でスマホから解きたい要求が近年高まっていた https://t.co/n6iMwl6NfR しばらくやってみよう | |
| #etaps2014 CC12件目:MSインターンによる https://t.co/KgfXU8XrNA の最適化の話。ベンチマーク収集にopt-inしたユーザのところで測定することで、どの環境でどの最適化が利くかの情報を収集して後に役立てるシステム。(続 | |
| #etaps2014 続) あと普通にその辺り詳しく考えたことがなかったので「JSに」コンパイルする言語の最適化パターンいろいろ集として割と面白かった | |
| @mizonokuchi おおー。面白い発表でした | |
| #etaps2014 CC13件目: ビジネスプロセスの検証をするツール。semantically equivalentだが「実行がしやすい」形に変換するのが普通の言語だけど、「検証がしやすい」形に変える変換をするコンパイラというものを考えてあれこれするぞーという話をしている | |
| #etaps2014 CC14件目: "Secure Two-Party Computation"（入力とプログラムを上手くencryptした論理回路にしてやりとりすることで、複数人からの入力をお互いに見せずにとって計算する系） にコンパイルするANSI Cコンパイラ。やばそう | |
| #etaps2014 Q:回路にコンパイルすることでnon-standard compilation problemが噴出しているの逆計算とかでもある状況だけどその辺どうよ？ （確かに楽しそう） | |
| 今日のセッションはここまで。おつかれさまでした | |
| #etaps2014 2日目 http://www.etaps.org/index.php/2014/programme/tuesday-april-8th の会場に来ています。あと論文へのリンク付きで昨日の分まとめた。適当に更新していきます http://togetter.com/li/652635 | |
| #etaps2014 FASE招待講演: マルコフチェインの辺にラベルを入れてラベルを選ぶ戦略schedulerを可変にしつつ重みも入れて重み和の届く限界で成り立つ性質みたいなものを時相論理とminとかmaxとかquantileとかの大小とか比とかで条件書けるモデル記述の検証技法 | |
| #etaps2014 盛りだくさんすぎて、schedulerとかquantileとか重み和とかがそれぞれどういう具体的な検証問題に対応するのかなどなど理解しきれなかった…。あとで復習しよう。だいたいの問題LPかLPの繰り返しに落ちるんだけど比が出てくるのが難しく今ホットと言ってた | |
| #etaps2014 ESOP1件目: APLやJのサブセットの静的型システムと意味論。これ系言語は配列の次元に関するpolymorphismがあって、関数がどの次元を演算単位としてとるかを元に処理が自動で高次元に自在にliftするんだけど、それで配列の形がどうなるか依存型で型付 | |
| #etaps2014 ESOP2件目: 基本型の上に付加情報として乗る型（Boost.Units的な単位型とか外部入力を表す"tainted"的情報とか）を、Gradual Type（動的/静的型ハイブリッドだが、型エラーが起きるなら絶対に動的エリアという理論保証が付く）でやる話 | |
| #etaps2014 J/APL/Jの話は、APL使いは、演算がこれならこの式はこれがこのように分割・拡張されてこういう演算が最終的に行われるということにすぐ慣れて使いこなします、といいながら驚異の次元合わせパズルを淡々と例で解説していってやばかった | |
| #etaps2014 gradual typing + hogehoge というのは、なんかhogehoge単体だとどうしても細かいケースで静的型がつけにくくて困ったところが実用上ある、みたいな過去の色々なトピックを放り込んで成立させるびっくり箱的使い方は将来性が確かにありそう | |
| #etaps2014 ESOP3件目: 超おもろかた。「この型の値は作れますか？」というクイズはカリーハワード的に「この命題証明できるか？」と同値。つまり逆に自動証明技術の転用で手持ちの部品の組合せで欲しい物を計算するソフト作れる？というプログラム自動合成になる…ここまで前提(続 | |
| #etaps2014 続)ただ、そのままでは部品を書いた言語内で合成を全部記述するのに対応するので、低水準言語の合成を高級言語のフルパワー表現力で行う用途に使えずつまらない。そこで、「この型のプログラムを生成するプログラム」という型をもったメタな体系"Staged計算"を使う(続 | |
| #etaps2014 続)Staged計算は様相論理と対応を持つので依然として話は筋を保っている。言語の型レベルでも高水準言語側で低水準側の精細化になるような型をふんだんにintersection typeで足すことで型ドリブン生成もよりはかどる、等々。とても楽しそうだった | |
| #etaps2014 冪乗を計算する以外のStaged計算の納得のいく使い道を個人的には初めて見た気分だ。探索で作ったコード片なんだけど生成先の言語が例えばクロージャがないとかのせいでなんかめんどい、みたいな状況結構あるのでそこでこう組み合わせるの、すぐにでも使いたみがある | |
| #etaps2014 ESOP4件目:「プログラミング言語の学び始めに"なんじゃこりゃー!!?"と思ったところも、 時間が経ってその言語に慣れると、当たり前になって気にしなくなってしまう。 だけど僕はそういう無心な引っかかりを大事にしたいんだ。」というイントロで発表が始まった(続 | |
| #etaps2014 続) 中身は特にAgdaのパターンマッチが順序付き・重なりあると上に書いたルール優先なのを滅ぼしたいという話だった（"="って書いてあるのに"="じゃないじゃないか！という初心を大事に）パターンのmguを右辺に適用した正規形が同じなら重なりを許すという解決策 | |
| #etaps2014 特にAgdaというのは定義に書いたequationが証明に使えるので特に証明記述言語だとoverlapping caseを持てるのは嬉しいということだと思う。「それCalculus of Algebraic Constructionと違うの？」て質問が出てた | |
| @rilakkumacho http://link.springer.com/chapter/10.1007%2F978-3-642-54833-8_5 これですー | |
| #etaps2014 POST招待講演 HiStar OS http://www.scs.stanford.edu/histar/ やその後の話。あらゆるリソースにラベルが付いててそれが流れる/ないの情報流の静的な検査で権限の漏れ等をチェックできるOS（その後ラベルから発展したモデルになってるらしい | |
| #etaps2014 FASE5件目: 分散システムを表現するモデル/代数の提案。各部分部分が違う粒度のクロックを持っている状態を表現できるのが新しいらしい。ふつうなことをふつうにやっている。 | |
| #etaps2014 FASE6件目: コンポーネントがマルコフ遷移として繋がっててそれぞれ１リクエストの処理時間情報が乗ってるモデルで、全体時間を解析する…際にモデルのパラメタ変更のバリエーションを記号表現して記号的に解いたら全ver一気に解けて嬉しいよという話。そうですね |