https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #ICFP 部分構造論理（各仮定をピタリ１回使わないとダメな線形論理、導入した順番通りに使わないと行けない論理etc）をTwelf http://twelf.plparty.org で表現する話：Judgement規則を完全にゴリゴリと書き下せばそれは書けるんだけど、(続 | |
| #ICFP 続)表現する論理の"変数"はそのままLFの"変数"になってないとTwelfの嬉しいところが発揮できなくて困るので、巧いこと変数を共用したまま埋め込むテクニックを開発。Twelfわからんのでわからんけど、割と素直にやってるように読める。(続 | |
| #ICFP 続) Ｑ：この埋め込みが正しいという証明は論文にはあるが、この証明自体をLFで書くことは？ Ａ：Twelfに元々無いXというロジックをYと表現した、という話でX⇔Yを証明するにはXを何かの形でLFで表現せねばならず結局その表現の正当性の証明が…というループになって無理 | |
| このtalkには @esumii さんの実況が欲しい… | |
| #ICFP ML風言語（型付きλ＋∀型＋∃型＋破壊的代入できる変数(1st order)＋破壊的代入できる変数(高階=関数とかも入る)）＋call/cc で書いたプログラムが等価である（どんな文脈に置いても必ず同じ振る舞いをする）ことを示すための新しい証明技法の話： 方法は(続 | |
| #ICFP 続) プログラムを状態遷移図として見てその遷移可能性で判断する？public transitionとprivate transitionというものを区別することで細かい区別ができるそうだ。"文脈はprivate遷移を起こせない"とするetc。よくわからなかった… | |
| #ICFP (let x = ref 1 in fun f => x=0; f(); x=1; f(); !x) 対 (fun f : ()->() => f(); f(); 1) の等価性は？という例題が使われていた。 | |
| ところで会場のディスカウント展示でConstraint Handling Rules http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521877763 という本が置かれてて面白そうなのですが、既に @ranha さん辺りが入手・品評済みであり面白いかどうか僕に教えてくれるといったイベントはありませんか？ | |
| #ICFP "NetFlixがリコメンデーションコンテストを取止め" http://www.wired.com/threatlevel/2010/03/netflix-cancels-contest/ こういうことが起きないようにする型システム： "Differential Privacy"という「特定レコードを除いても同じ結果になる確率が微少しか変化しない」クエリを | |
| #ICFP 安全。適宜ノイズを加えてこの安全性を達成しなさい、と定義するモデルがあるんだけど、それを型で検証。"これしか確率変わらない"的な型。線形型システムに似るらしい。便利にプログラム組むのに、add_noiseできたり確率を裏で管理してくれるプライバシーモナドも作ったよ、と | |
| #ICFP こういうのって、例えば暗黙に相関してる値とかがあるときにうっかりリークしたりしないのかなあ…というのはきっとちゃんと考えられているんだろうけど、それに限らず、細かいところまで理解できてないと、どこまで信用して運用すればいいのかが難しそうだなーという気がする | |
| @ranha ありがとうございます！型推論への応用とかよりはわりと純粋にCHRに興味があるので良さそうですね。さて買うか… | |
| #ICFP 依存型でセキュリティ型： アクセス権限の認証とかに「権限を持ってることの証明」をやりとりするプロトコルがあって、それを依存型のある言語（Agda）の型で実現。「Judgement規則を完全にゴリゴリと書き下す」埋め込みみたい。 | |
| #ICFP 「双方向変換」３連。データベースのview update等が例ですが、「データsを加工してデータvを出力する関数f」に対して「出力vを編集したらその編集を適切に入力sに書き戻す」計算bwを自動導出する！研究。適切とはbw(s,f(s))=s&f(bw(s,v))=v | |
| #ICFP 松田らの構文的手法(ソース解析して「fが取り出さなかったsの情報」を計算する補関数f'を導出し、bwはそれをガイドに編集を反映)とVoigtlaenderの意味的手法（http://www.kmonos.net/wlog/93.html#_0901090117 パラメトリシティのお陰でメタ計算無しの逆向き導出）の融合： | |
| #ICFP 意味的手法はデータ構造（ツリー等）のノードに格納された"値"の編集の反映はとても簡単だけど、ツリーの"構造"自体の変更に対応できない。構文的手法は逆に構造の変更に強い。強みを合わせるべく、fを"構造"の加工と"値"の加工部分に分離＆それぞれ得意な方を使って双方向化！と | |
| #ICFP Matching Lense：このグループはLenseというコンビネータベースの双方向化をやってる。fと補関数f'とbwの３つ組が予め定義されたプリミティブ処理を組合せることで双方向可能な色んな複雑な変換を記述できるもの。今回の論文は"alignment"問題への対処 | |
| #ICFP alignmentというのは、ユーザが出力vを並び替えたような時に、彼らの枠組みでは"ユーザがどういう編集操作をしたか"(operation-based)はわからないという前提で"編集後のデータv'だけがわかる"(state-based)という仮定で逆化してるので(続 | |
| #ICFP 続)元データsに戻すときに元あったのと無茶苦茶な順番に書き戻してしまう問題。これを、まずfとf'の間のリンクを覚える＋（適当なヒューリスティックス（diff風、set風など）を選んで）編集前vと編集後v'のマッチングを計算→それに従った位置に戻す、という解決策 | |
| #ICFP Syntactic&SemanticのやつのHackageがあるのかー http://hackage.haskell.org/package/bidirectionalization-combined | |
| #ICFP BiG：代数的データ型（≒ツリー）だけじゃなくグラフ操作の双方向化もやろうぜという話。共著者とかしてます。グラフの厄介なところは、今朝の教育の話じゃないですけど、ヤツらはあまり"inductive"でない（明確に部分と部分に分かれず全体がごちゃっと関係してる）とこで、 | |
| #ICFP 続)でもそこを巧く（例:オートマトンのε遷移に似たε辺の仮想的導入など）inductiveに見せてグラフ処理できるUnQL http://portal.acm.org/citation.cfm?id=765224 って言語があって、この子の意味論を注意深く強化してくと双方向化の技術もグラフの上に上手く乗るよ！と。 | |
| #ICFP Fresh name：「プログラム/証明中でλ式などを表現する時"変数名"をどう扱うか問題」の話。スコープ間の親子関係を幽霊型で表現することで不正な名前処理ができないように、という理解でよいのかな…なんだかすごく当たり前に見えるので聞き逃してることがありそう… | |
| #ICFP トークのメモ書き終わってないけど Award などなど Session が始まっている。 | |
| #ICFP 2011年のICFPは東京開催。会場は NII ( http://www.nii.ac.jp )。SIGPLANの会議がアジアに来るのは始めてらしい。(via http://twitter.com/esumii/status/25822145063 ) | |
| #ICFP 「10年前のICFPの論文で最も後世への影響が大きかったで賞」 goes to QuickCheck！ http://doi.acm.org/10.1145/351240.351266 | |
| #ICFP （いわずもがなの注釈）QuickCheck とは Haskell のランダムテストライブラリです。参考URL： http://madscientist.jp/~ikegami/diary/20060906.html http://itpro.nikkeibp.co.jp/article/COLUMN/20080304/295346/ http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck | |
| #ICFP コンテスト参加チーム871（自己申告のあった国別内訳：USA 29 Japan 28 Russia 25 Germany 12 Ukraine 11 …）（言語：Haskell 29 C++ 17 Python 16 Java 12 OCaml 7 Ruby 6…） | |
| @esumii あ、本当ですね。すみません | |
| #ICFP まちがえた。アジア初ではないです： http://twitter.com/esumii/status/25823436822 | |
| #ICFP コンテスト Judge's Prize: theCult of Bound Variables (SML,C++) (actually also used Python,Mathematica,AMPL,Perl,bash,PHP) | |
| #ICFP コンテスト Lightning： Carl Witty (Sage http://www.sagemath.org/ ) | |
| #ICFP コンテスト 2010 Winner！ Pure Pure Code ++ (C++, Haskell, Python, ...) http://twitter.com/nya3jp/status/16604202811 ！！！！！ | |
| で、結局今年悪口を言ってはいけない言語はどれになるのでしょうか！？＞ぴゅあぴゅあの皆様 | |
| 風邪を引いているような気がする | |
| #ICFP HtDP方式のプログラミング教育の話その２：進度に応じて、言語自体の機能量を変えていく"language level"というやり方が肝。教えてない言語機能は使われないだけでなくて、そもそもその機能がないシンプルな言語で教えて段々言語自体を強化してく。(続 | |
| #ICFP 続)Schemeベースですしその程度の言語改変は余裕だ、ということかな。進度に応じて小さい言語を使うことで、暗号のようなエラーではなく適切なエラーを"出せる（例:"lhsでない式には代入できません"<<<"変数じゃないと代入できません"）というのが初学者には非常に重要 |