https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #PPDP11 "Maintaining Distributed Logic Programs Incrementally" Datalog（関数記号なしProlog、関係代数とはまた別のデータベースの理論のベースなどとして使われる）上の分散プログラムで、元データの更新を (続 | |
| #PPDP11 続) 変な状態に行ったりループしたりしないよう全体に浸透させるアルゴリズムの話。既存研究(ICDE09,SIGMOD06)はモデルが制限されすぎで現実と遠い、と。viewを適切に更新してくというのはself adjusting computationとか近いのかな | |
| #PPDP11 "CLP Projection for Constraint Handling Rules" タイトル通り。CHRをCLP(Constraint Logic Programming)にマップしてそっちで研究された解析手法色々を色々適用するよーという話。 | |
| Coinductive 眠気 | |
| #PPDP11 "Towards Automatic Synthesis of Software Verification Tools" 招待講演3。パーサを書くのにはパーサジェネレータがあるように、VerifierにもVerifier generatorを！という筋のお話 (続 | |
| #PPDP11 続) プログラムの表す"導出規則"（このステートでこうなら次のステートではこうなる）を与えると、それの検証に必要な不変条件を見つけてきてくれたり。バックエンドはHorn節ベースの表現で+SMT+CEGAR。いまいちこれで検証器生成器、というイメージが湧かないむう | |
| @cpp_akira はい、今晩ちゃんとしたスケジュール練ります……。 / どうしよう。COMFRK監禁致死大会 http://atnd.org/events/13077 に自ら混ざって関係のない原稿を死と対面しながら書くとか…… | |
| #PPDP11 "Typing Control Operators in the CPS Hierarchy" callccの上にshift/resetが現れるその関係を何度も繰り返すとレベルN shift/reset、限定継続の階層ができますが、その(単相)型システムを提案(続 | |
| #PPDP11 続)型の詳細(特に先行研究との差分)は全然理解できてないのですが、提案プリミティブがLV1～nまでの継続を一気に捕捉L(k1,…,kn).tと一気に継続をスタックに積み上げ(k1,…,kn)←tという物で、表現力同じらしいけど考え方としてこれ面白い考え方できるかな | |
| #PPDP11 "Dependent Session Types via Intuitionistic Linear Type Theory" タイトル通り。依存型でセッションを型付け。「10以下と証明されている整数を送る」とか「ソート済みのリストを受け取る」とかそういう型。 | |
| #PPDP11 "Recursion in a linear typed lambda-calculus" Linear λ計算（各変数をかならずちょうど１回ずつ使うλ計算）に自然数のペアをカウンタとして使う再帰ができるプリミティブを足した物はTuring完全に。(続 | |
| #PPDP11 続) 再帰は再帰プリミティブの中で同じものが繰り返され色々なことができちゃうので、それはそうだろ、というか、線形とは何だったのか、という気分だけど、方向としては、依然として構文的には＆色々な意味で線形ではあるので実装は楽で、つまり中間言語として使えるのでは等々。 | |
| #PPDP11 "Nested Proof Search as Reduction in the lambda-calculus" 「論理と計算の対応に二大アプローチがある。証明の正規化を計算と見る(関数型プログラミング)か、証明の探索を計算と見る（論理型プログラミング）か」(続 | |
| #PPDP11 続)この研究は、まるでλ計算のように見えλ計算のように動いているが裏では証明の探索と対応している、λs (λ計算 with explicit substitutions)というシステムを提案。とても面白そう＆論文も見た感じとても読みやすく整理されてるので (続 | |
| #PPDP11 続) これはあとでしっかり読んでみよう。発表は、ひたすら導出規則が並んでいるのを見て証明探索っぽい夏の風情を感じようというものでしたがその境地には至れなかった…。基本、((A→B)→C)→D├A→((B→C)→D) のような→のカッコ付け替え則が探索っぽいのかな。 | |
| #PPDP11 lambda-sigma? と本質的に同値、という質疑が行われているが詳細理解できてない | |
| #PPDP11 #LOPSTR11 おしまい http://twitpic.com/5txcny | |
| まとめました。 http://togetter.com/li/164644 |