jssst sig-ppl

第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
プログラム

1日目午後の部 (3月4日 13:45-18:30)

13:45-13:50 オープニング
13:50-15:05 セッション1 関数型言語1 (座長 南出 靖彦 (筑波大学))
Cとの連携機能を持つ関数型言語におけるプロファイラの試作 [C1]
朝井 雄大(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学情報科学研究科 (2)東北大学電気通信研究所)
概要  本論文では,我々がSML#のために開発したプロファイラの試作について報告 する.プログラムの動的な振る舞いを解析するプロファイラは,高品質のソフトウェア を開発するにはなくてはならないが,これをスクラッチから実装するには多大な労力を 要する.また,SML#のもつC 言語との相互運用をふまえると,C とML のコードが混 在したプログラムに対して適切なプロファイル結果が得られることが望ましい.このよ うな立場から,既存のC 言語向けプロファイラであるgprof をベースにし,SML#のプ ロファイラを設計・試作した.予備的な評価実験の結果,この試作が性能改善に有用であ りうることが確認できた.また,関数型言語特有の興味深い挙動もいくつか発見された.
shift/reset によるモナドトランスフォーマの提案と実装 [C1]
金子 ちひろ, 浅井 健一 (お茶の水女子大学)
概要  近年、OchaCaml などの開発環境が整ってきており、shift/reset のさらなる 応用が期待されている。Filinski はモナドをshift/reset で表現することで、従来のモ ナド形式によるエフェクトが、直接形式のプログラムで扱えることを示した。本論文で は、直接形式のプログラムでエフェクトを組み合わせる手法として、Filinski の表現に 対するモナドトランスフォーマを提案する。本論文のアイデアは、直接形式で継続の戻 り値(アンサータイプ)となっているモナドに着目し、トランスフォーマの機能をアン サータイプの変換として表現することである。このアイデアに基づき、各種のトランス フォーマについてOchaCaml による実装を行った。今後の課題として、提案手法の性質 および正当性について議論する。
分割統治計算可能性の多相型を用いた保証 [C1]
森畑 明昌 (東北大学電気通信研究所)
概要  本論文では、目的とする計算が「入力を複数に分割し、それぞれに対し並列に 計算を行い、結果を併合する」ことによって達成できるか否かを知ることを目標とする。 この話題に関しては第三リスト準同型定理(Gibbons, JFP 1996) が知られている。この 定理によれば、リストに対する計算がある2 形式の逐次処理として記述できることが、 リストを分割した各断片を並列処理できるための必要十分条件である。本論文ではこの 定理を一般化し、リストに限らず入力を複数の値に分割したとき、それらに対する並列 計算の結果から所望の値を得ることができるための必要十分条件を示す。この条件は一 般的ではあるが実用上は使いづらい。そのため、これに加え、分割結果を分割前の値へ と併合する関数がある種の多相型をもつならば、特定の2 種類の形式のプログラムの存 在が分割統治並列計算存在の十分条件となることを示す。さらに、この一般化の意義に ついて、いくつかの例を通して確認する。
15:05-15:20 休憩
15:20-16:20 セッション2 招待講演1 (座長 権藤 克彦 (東京工業大学))
数値計算のための大規模並列プログラムの自動生成
村主 崇行 (京都大学)
概要 偏微分方程式を陽的に解く大規模並列プログラムを自動生成するためのドメイン特化型言語であるParaisoについて発表します。 Paraisoは、関数型言語Haskellに埋め込まれた言語であり、実装したいアルゴリズムを、型レベルテンソルやコンビネータを用いて簡潔に、 かつ、衝撃波解法・空間補間法・時間積分法などの要素を自由に組み合わせ可能な形で記述することができます。 また、マルチコアCPUおよびGPU向けのコードを生成することができ、なおかつ生成したコードの性能に対して遺伝的アルゴリズムを利用した自動チューニングを施すことができます。 2次精度のNavier-Stokes方程式ソルバを生成して自動チューンした結果、マルチコアCPUにおいては広く使われている既存のソルバと遜色ない性能を、GPUにおいてはそれを10倍程度上回る性能を出すことができました。
16:20-16:30 休憩
16:30-17:15 セッション3 遷移系と木変換器 (座長 中野 圭介 (電気通信大学))
Conditional Transformable Pushdown System: スタックの変換と検査が可能なプッシュダウンシステム [C1]
上里 友弥(1), 南出 靖彦(2) ((1)筑波大学情報学群情報科学類 (2)筑波大学システム情報系情報工学域)
概要  プッシュダウンシステム(PDS)はスタックを備えた計算モデルであり,再帰 的なプログラムの解析などに用いられて来た.また,より複雑な解析の為にスタックの 検査が出来るConditional PDS と,スタックの変更が出来るTimed PDS などが提案さ れ,それぞれPDS へ還元出来ることが示されている. 本論文では,これらConditional PDS とTimed PDS を統一したような,スタックに対 する検査と変換の両方を行うことの出来る計算モデルであるConditional Transformable PDS(CTPDS)と,これを形式化する為に用いるトランスダクション規則で拡張した PDS(TrPDS)を提案する.特にTrPDS からPDS への変形により,CTPDS 上の位置 到達可能性問題が決定可能であることを示す.
Determinacy and Subsumption of Single-valued Bottom-up Tree Transducers [C2]
Kenji Hashimoto(1), Ryuta Sawada(2), Yasunori Ishihara(2), Hiroyuki Seki(1), Toru Fujiwara(2) ((1)Nara Institute of Science and Technology (2)Osaka University)
出典: 7th International Conference on Language and Automata Theory and Applications (LATA 2013) (掲載予定)
17:15-17:25 休憩
17:25-18:30 セッション4 高階モデル検査 (座長 田辺 良則 (国立情報学研究所))
Exact Flow Analysis by Higher-Order Model Checking [C2]
Yoshihiro Tobita(1), Takeshi Tsukada(1), Naoki Kobayashi(2) ((1)Tohoku University (2)University of Tokyo)
出典: Eleventh International Symposium on Functional and Logic Programming (FLOPS2012) (掲載済)
高階モデル検査器TRecSの効率化 [C1]
伊藤 宗平, 小林 直樹 (東京大学大学院情報理工学系研究科コンピュータ科学専攻)
概要  高階再帰スキームのモデル検査は関数型プログラムの検証に有用な技法である. この問題の最悪時間計算量は多重指数時間完全であるが,典型的な入力について効率よ く動作する実践的なアルゴリズムが存在し,モデル検査器TRecS に実装されている. このアルゴリズムではスキームを実際に展開しながら型環境を推定することを,スキー ムの型付けに十分な型環境が得られるまで行う.TRecS を利用したプログラム検証ア ルゴリズムも提案・実装されており,様々なプログラムの自動検証も可能となったが,モ デル検査器の更なる効率化がプログラム検証の適用可能範囲を広げるために必要である ことも明らかになった.本論文では,型推論時の失敗情報に基づいてスキームの展開候 補を定めることで,目標指向的に型環境の推定を行う手法を提案・実装し,その有用性 について報告する.
Two-Level Game Semantics, Intersection Types, and Recursion Schemes [C2]
C.-H. Luke Ong(1), Takeshi Tsukada(2) ((1)University of Oxford (2)Tohoku University)
出典: The 39th International Colloquium on Automata, Languages and Programming (ICALP 2012) Track B (掲載済)

1日目夜の部 (3月4日 20:30-22:00)

20:30-22:00 セッション5 ポスター・デモ1
Coq による PostScript プログラミング [C3 (ポスター・デモ)]
坂口 和彦 (筑波大学 情報学群 情報科学類)
概要 定理証明器 Coq を用いて PostScript 言語のサブセットを定義し、その言語のための開発環境を Coq の proof editing mode の上に実装する方法について発表する。この開発環境の特徴は、プログラムの十分に一般化された実行中の状態を見ながらプログラムを書けるという点にある。また、この開発環境は直感的な仕様記述からプログラムを自動生成する機能や、記述したプログラムの PostScript プログラムへの変換・埋め込みをサポートし、ブール値や自然数を扱うためのライブラリを持つ。デモではこの開発環境を実際に動かし、プログラムを記述する方法を説明する。
動的に変化するグラフのための効率的な一意エンコード生成手法 [C3 (ポスター)]
宮原 和大, 上田 和紀 (早稲田大学)
概要 グラフ構造を扱うプログラミング言語にモデル検査機能を実現する際, 多くのグラフ同型性判定を行うため判定の効率は重要である. グラフからの一意的なエンコード生成は エンコードの比較による同型性判定を可能とし, 多数のグラフ間での判定の際に探索回数の削減を可能とする. また,現実の構造をモデル化したグラフは その構造の時間に伴う変化によりグラフも動的に変化する. 特に変化が部分的であれば変化の前後でグラフの構造は大部分が保存され, 変化前の構造から変化後の構造を推測できる. 本研究では動的に変化するグラフについて, 変化前の構造のエンコードの利用により 変化後の構造のエンコードを効率的に再計算する手法の提案を行う.
LMNtal処理系SLIMのマルチスレッド化による最短経路問題のデータ並列求解 [C3 (ポスター)]
青山 龍一, 上田 和紀 (早稲田大学)
概要 LMNtalは階層グラフ書き換えに基づく並列言語モデルである. LMNtalの実行時処理系としてSLIMが近年開発されている. SLIM は従来の実行時処理系と比べて軽量化かつ高速化に成功したが, 今後大規模なデータを扱うためにはグラフ構造のデータ並列書換えの技法を確立する必要がある.そこで本研究では, POSIXスレッドを使って, SLIMのデータ並列化の実装を行った. そしてLMNtalによって書かれたネットワークの最短経路問題のプログラムに対して並列化の実装を行ったSLIMを実行し, 並列効果が出ているかを検証した.
SLIMの階層グラフのためのキャッシュコンシャスかつ効率的なデータ構造 [C3 (ポスター)]
吉田 健人, 上田 和紀 (早稲田大学)
概要 階層グラフ書換えに基づく状態遷移系記述言語LMNtalの実行時処理系SLIMはLTLモデル検査機能を備えている.LTLモデル検査は状態空間の構築処理を伴うが,SLIMの状態空間構築は階層グラフのバイト列圧縮やハッシュ値計算等の処理がボトルネックになっている.状態空間構築の各処理の高速化のために,階層グラフのキャッシュミスを減らすことが重要である.そこでメモリプールを用いてキャッシュブロックのプリフェッチの効果を増し,メモリコストの少ないデータ構造に変更することでキャッシュの実効容量を増大させた.本研究により各処理の単体テストにおいて最大で2.2倍程度速度向上が見られた.
線形純粋型理論 [C3 (ポスター)]
木村 大輔 (国立情報学研究所)
概要 本発表では純粋型理論 (Pure Type System) の線形論理変種である線形純粋型理論を提案する.純粋型理論は単純型付ラムダ計算やSystem F, 依存型システムなど様々な型理論を提供する一般的なフレームワークである.線形論理は直観主義論理を分析する様々なアプローチを提供してきたが,これと同じように線形純粋型理論による純粋型理論を分析する新しいアプローチを提供すると期待できる.
LMNtal並列モデル検査における状態生成数削減及び高速化 [C3 (ポスター)]
安田 竜, 上田 和紀 (早稲田大学)
概要 階層グラフ書き換え言語LMNtalの実行時処理系であるSLIMには,プログラムの検証を行うモデル検査機能が実装されている.モデル検査とは,状態遷移系としてモデル化されたシステムを網羅的に探索することによって,そのシステムが要求された性質を満たすかを判定する手法である.SLIMで採用されているMAP,OWCTY等の並列モデル検査アルゴリズムは,エラーを含む問題に対して状態生成数が多くなるほか,特定の問題に対して極端に性能が落ちるという問題を抱えている.本研究では,これらの問題を解決するため,新たなアルゴリズムの設計と実装を行い,その性能を評価した.
Glasgow Haskell Compilerが提供するIOマネージャの並列化 [C3 (ポスター)]
山本 和彦 (株式会社IIJイノベーションインスティテュート)
概要 GHC(Glasgow Haskell Compiler)は、理想に近いネットワーク・プログラミング環境を提供している。すなわち、イベント駆動プログラミングで実装された IO マネージャがコアの性能を引き出し、プログラマは軽量スレッドを使って見通しのよいコードを記述できる。しかし、IO マネージャは1つしか存在しないので、マルチコアの性能を引き出せないという問題があった。我々は、1つのプロセス内で、IO マネージャをコアの数だけ起動して、すべてのコアの性能を引き出すよう改良した。このポスターでは、問題の詳細と実装のキーアイディアについて説明する。
型レベルプログラミングを用いたCoqからHaskellへのプログラム抽出 [C3 (ポスター・デモ)]
中村 宇佑 (東京大学情報理工学系研究科コンピュータ科学専攻(萩谷研))
概要 定理証明器Coqにはプログラム抽出という機能があり、Coqのプログラム部分をO'CamlやHaskellのプログラムに変換できる。しかし現在のCoqの抽出機能では一度ML(miniml)に変換しているため、MLで型付けできない第一級型や依存型を扱うことができない。それに対しHaskellには型レベルプログラミングという手法があり、第一級型や依存型に近い物を扱うことができる。本研究では型レベルプログラミングを用いたCoqからHaskellへの抽出について論じる。PPL2012ではこの抽出の可能性を関係データベースの例を用いて示した。本ポスターでは具体的な抽出方法について述べる。
Dialectica解釈と双方向変換とのCurry–Howard対応 [C3 (ポスター)]
浅田 和之 (国立情報学研究所)
概要 Dialectica解釈はGödelによってHeyting算術の無矛盾性を量化子のないSystem Tへ帰着させるために導入された。一方、双方向変換は変換したデータへの編集を変換前のデータに自動的に反映させる手法として研究され、近年、双方向変換を記述するための言語の研究がプログラミング言語の研究分野で行われている。双方向変換ではGetPut及びPutGetという公理が要求されることが多いが、本研究ではDialectica解釈とGetPutを満たす双方向変換との間にCurry–Howardスタイルの対応関係があることを示し、また同様のフレームワークでPutGet公理をどのように表現するかを示す。そしてこの対応を通して双方向変換言語を拡張する。
JavaScript処理系に対する外部関数インタフェースの設計及び実装 [C3 (ポスター)]
谷村 明, 岩崎 英哉, 中野 圭介, 鵜川 始陽 (電気通信大学)
概要 近年,JavaScript(JS)が,Webアプリケーションのサーバサイド開発に用いられるようになった.サーバサイドでの開発では,他言語のプログラムとの連携を行いたいという要求がある.これを解決するには,外部関数インタフェース(FFI)を利用するのが一般的である.既存のJS処理系のFFIでは,記述性や機能面に問題がある.本研究では,Cで定義された関数をJSから呼び出すためのFFIを設計し,これを現在開発中のJS処理系上に実装した.本研究で実装したFFIと既存処理系のFFIで,利用できる機能を比較したところ,本研究によるFFIは,C側で利用できるJSの機能が充実していることがわかった.
データフロー要約の構文主導型並列計算 [C3 (ポスター)]
佐藤 重幸(1), 森畑 明昌(2) ((1)電気通信大学 (2)東北大学電気通信研究所)
概要 これまで,データフロー解析を並列化する研究が行われてきているが,少数の巨大な手続きから構成される入力プログラムに対して,負荷分散を行うには不十分である.望ましい並列アルゴリズムは,プログラム全体に対する分割統治である.しかし,データフロー解析は,複雑なデータ依存性を伴った反復法による不動点計算を要するため,分割統治型の計算を抽出するのが難しい.本研究では,whileループなどの構造的制御フローと,gotoなどの非構造的制御フローを区別し,前者のデータフローを分割統治によって並列に要約する手法を示す.本手法による解析器を,COINS上で簡易的に実装し,予備的な実験を行った.本研究は進行中である.
LMNtalコンパイラの検証に向けたグラフ書き換え操作の形式化 [C3 (ポスター)]
信夫 裕貴, 上田 和紀 (早稲田大学)
概要 LMNtalは階層グラフ書き換えに基づく言語モデルであり、並行計算や多重集合書き換えなどの計算モデルの統合を目指している。LMNtalプログラムはコンパイラによって中間命令列に変換されるが、命令の動作やコンパイルの正当性については十分な形式化が行われていない。プログラムの動作保証のためには、コンパイラ検証が重要な課題である。そこで、グラフ書き換えをリンク列の置換と捉えたコンパイル手法を提案し、実装した。これによって書き換え命令と命令生成の形式化を行い、証明支援系Coqによる形式的検証を目指す。本発表では、提案手法とその実装、CoqによるLMNtalコンパイラの検証に向けた展望について述べる。
SIMT プログラムのためのホーア論理 [C3 (ポスター)]
小島 健介, 五十嵐 淳 (京都大学・JST CREST)
概要 SIMT (Single Instruction Multiple Threads) は,GPU プログラミングのために設計された NVIDIA の並列プログラミングモデルである。本発表では,SIMTプログラムの正しさを推論するためのホーア論理を提案する。まず,実際のSIMT を簡略化したモデルを考え,これを while 言語の拡張として定式化する。次に,ホーア論理の構文と推論規則を与え,それが適当な条件を満たすプログラムに対して健全性および相対完全性を満たすことを示す。
データベースを用いたMikiβの拡張に向けて [C3 (ポスター・デモ)]
中野 祥, 浅井 健一 (お茶の水女子大学)
概要 Mikiβとは証明木を書くための汎用的なGUIライブラリである。Mikiβの作成したGUIでは、あらかじめ推論システムとして定義した規則のみが利用可能である。しかし証明木の構築においては推論システム上の規則だけではなく、証明が完了した木を新たな規則として他の証明を行う際に再度利用したいという要求が存在する。本研究ではデータベースとphpを用いて証明木データの保存・読み出しを行うことにより、証明木の再利用を可能にすることを目的とする。
適用する破壊的クラス拡張を実行時に切り替えるモジュールシステムMethod Shells [C3 (ポスター)]
竹下 若菜, 千葉 滋 (東京大学 情報理工学系研究科 創造情報学専攻)
概要 本研究では,適用する破壊的クラス拡張を,プログラムのコンテキストに応じて実行中に切り替えるモジュールシステムMethod Shellsを提案する.ライブラリを拡張する際,ソースコードを直接書き換えずに差分のみを別ファイルに記述することでメソッド定義を変更できると便利である.破壊的クラス拡張と総称できる,このようなメソッド定義の変更機構は,これまで様々な言語に実装されている.しかし同じクラスに対する破壊的クラス拡張を複数適用すると,同じメソッド定義が複数存在する可能性がある.Method Shellsは適用する破壊的クラス拡張を実行中に切り替えることでこれを防ぐことを可能にした.
HPCアプリケーション最適化に伴う計算漏れ検出手法の検討 [C3 (ポスター)]
穂積 俊平, 佐藤 芳樹, 千葉 滋 (東京大学大学院 情報理工学系研究科 創造情報学専攻)
概要 計算漏れを検出するための開発ツールを提案する。HPCの分野では、最適化のために計算順序を変更する事がある。計算順序を変更する事で、キャ シュヒット率の向上や、データ転送と計算のオーバーラップを達成できる。しかし、計算順序を変更する際に計算範囲を誤ってしまい、計算漏れが発生 する事がある。計算漏れを検出する事は難しい。プログラムが停止しない事があり、この場合間違っているコードを特定しがたい。また、HPCでは小 数点演算を繰り返すため、誤差の蓄積が大きく、計算漏れとの区別が付きにくい。この発表では、計算漏れの原因とそれに対する対応を示す。
メソッドのオーバーライドにより部分的実行順序が定義可能なHPC向け言語 [C3 (ポスター)]
宗 桜子, 佐藤 芳樹, 千葉 滋 (東京大学 情報理工学系研究科 創造情報学専攻 千葉研究室)
概要 本研究では、メソッドの部分的な実行順序が定義可能なHPC向けプログラミング 言語を提案する。 並列分散処理を用いたステンシル計算では、グリッドの一部では他の領域と異な る計算を行う必要がある。 しかし、JDK8で導入される並列コレクションでは、 領域毎の処理の違いや、その実行順序を定義する機能が提供されていないため、 その利用者はアプリケーションの最適化を十分に行えない。 この問題に対し、我々はメソッドをオーバーライドすることで部分領域を指定す る構文を導入し、 あるクラスのメソッドに対して、異なるバージョンを定義できる機能を追加する。 これにより、プログラマは部分領域を指定し、各部分領域毎に異なる計算内容を 記述する事ができる。
バックトラックによる正規表現マッチングの時間線形性判定 [C3 (ポスター)]
杉山 聡(1), 南出 靖彦(2) ((1)筑波大学 システム情報工学研究科 コンピュータサイエンス専攻 (2)筑波大学 システム情報系 情報工学域)
概要 現在広く使用されているperl互換の正規表現の実装では、マッチングの計算量が文字列の長さに関して指数関数的になりうる。さらに、バックトラックが一定回数を超えるとマッチングを打ち切る実装となっており、本来マッチすべき文字列にマッチしない可能性がある。本研究では、正規表現を受けて、その正規表現によるマッチングの計算量が線形かどうかを判定する方法を考案した。正規表現を木構造で形式化し、それの持つ性質を使って判定する。実際に使用されている正規表現を対象に実験を行い、計算量が線形でないと判定されたものに対して、マッチングに指数関数時間要するかを調査した。
An Accumulative Computation Framework on MapReduce [C3 (ポスター)]
劉 雨(1), 江本 健斗(2), 松崎 公紀(3), 胡 振江(4) ((1)総合研究大学院大学複合科学研究科 (2)東京大学情報理工学系研究科 (3)高知工科大学情報学群 (4)国立情報学研究所アーキテクチャ科学研究系)
概要 MapReduce is a very popular parallel programming model which dramatically simplifies the large scale data processing. In spite of the simplicity of MapReduce, there are still lots of algorithms which cannot be implemented by MapReduce easily, because they are hard to be divided into independent sub-computations due to their innate characters of computational dependency. In this presentation we propose a systematic approach to handle a large class of such difficult computations by MapReduce, based on a useful and general computation pattern named accumulate. We describe an efficient algorithm for parallel accumulate and implement a framework which adapts high level abstraction of the accumulate pattern to MapReduce and provides generic and functional style programming interfaces. Instead of writing low level MapReduce literatures, users only need to write functional idioms which define the computations. Our experiments show the usefulness and efficiency of our framework.
動的レイヤー合成のための型システム [C3 (ポスター)]
井上 裕昭(1), 五十嵐 淳(2), Robert Hirschfeld(3), 増原 英彦(4) ((1)京都大学工学部 (2)京都大学大学院情報学研究科 (3)Hasso-Plattner-Institut Potsdam (4)東京大学)
概要 動的レイヤー合成は,複数のクラスにまたがるメソッド定義の集まりであるレイヤーを有効化・無効化することによりオブジェクトの挙動を動的に変更するための言語機構であり,文脈指向プログラミング言語の主要な機能のひとつである.レイヤーは既存の挙動を変更するメソッドだけでなく,新たなメソッドを含むこともあるため,有効化・無効化によりオブジェクトのインターフェースは動的に変化する.本研究では,動的レイヤー合成の安全性を保証する型システムを与え,その型健全性を証明する.これにより,呼び出されたメソッドが実際に存在することだけでなく,レイヤー有効化前の挙動を呼び出す機能である proceed 呼び出しが失敗しないことも保証できる.
オーダー2の高階ブーリアンプログラムの文脈等価性に関する同値類列挙 [C3 (ポスター・デモ)]
長井 雅比古(1), 住井 英二郎(2) ((1)東北大学工学部情報知能システム総合学科 (2)東北大学大学院情報科学研究科)
概要 「ブール型と再帰を含む名前呼び単純型付きラムダ計算を対象として、オーダー2の与えられた型のプログラムを(文脈等価なものを除き)全て列挙するアルゴリズムを与える。伊藤・小林[2012]はオーダー2のプログラムの文脈等価性を判定するため、オーダー1のプログラムを列挙するアルゴリズムを与えた。本研究ではオーダー2のプログラムを列挙することにより、オーダー3のプログラムの文脈等価性や安全性の判定を可能にする。例えば、bool→bool型の二つの引数の関数合成は、素朴には高々11^121通りありうるが、本研究ではそれを354通りに特定することができた。発表では実装に関するデモも行う。」
高階再帰スキームのための交替性パリティ木オートマトンモデル検査器 [C3 (ポスター・デモ)]
藤間 幸一(1), 伊藤 宗平(2), 小林 直樹 (2) ((1)東京大学理学部情報科学科 (2)東京大学大学院情報理工学系研究科)
概要 高階再帰スキーム (HORS)は無限木を表す高階文法であり,そのモデル検査問題とは,HORSと木オートマトンを入力とし,HORSの生成する木がオートマトンによって受理されるか否かを判定する問題である.この問題は極めて高い計算量を持つが,近年現実的なモデル検査器が実装され,プログラム検証に応用されている.しかしながら,既存のHORSのモデル検査器は,自明木オートマトンや交替性弱木オートマトンと呼ばれる限られた木オートマトンを対象としていた.そこで本研究では,木オートマトンのクラスを交替性パリティ木オートマトン(APT)に拡張し,それに対する現実的なHORSのモデル検査アルゴリズムを考案し,実装した.発表ではアルゴリズムの説明とともにデモを行う.
通信プロトコル仕様の形式化による形式検証とファジングテストへの応用 [C3 (ポスター・デモ)]
大岩 寛, Reynald Affeldt (AIST)
概要 RFCなどに定義された既存の実用通信プロトコルの仕様は、多くの場合英語などの自然言語を援用して記述され、形式検証や実装の検査にそのまま用いるのは困難であることが多い。このことは実装の不具合の原因となるだけでなく、検証・テスト結果の信頼性にも影響する。 本研究では、既存記述の持つ可読性を最大限維持しつつ、実装に十分な詳細さを備えた形式仕様記述言語を設計、実際のTLSプロトコルの仕様記述に適用した上で、実装の正当性の形式検証や実装のブラックボックス検査に応用する。 仕様記述からの形式検証への適用の詳細と、本仕様記述から検査器を自動生成し、TLSプロトコルの既存実装に対して網羅的な動作検査を行なうシステムを展示する。
Metamorphism in Jigsaw [C3 (ポスター; C2から移動しました)]
中野 圭介 (電気通信大学 先端領域教育研究センター)
出典: Journal of Functional Programming (Cambridge University Press) (後日掲載予定 オンラインでは掲載済)
概要  関数型プログラミングにおいて,リストを消費する関数 foldr とリスト を生成する関数 unfoldr は重要な役割を果たしている. 特に,入力を foldr によって消費し,出力を unfold によって生成するような関数はメ タモルフィズム (metamorphism) とよばれ,基数変換などに代表されるデー タ表現間の変換を自然に定義することが可能である. Bird と Gibbons は,このメタモルフィズムに対し,入力を 消費しながら出力を生成する ようなストリーム処理として実装できるための条件を提示したが,自然数 に対する基数変換には応用することができなかった.これは入力の桁を全 て読み込まない限り,出力の桁を決定できないためで,彼らの提示した条 件を満たしていない.本研究では,ジグソーパズルを利用したメタモルフィ ズムの計算機構を提案し,その機構が適用できるための条件を示す.本計 算モデルは,基数変換だけでなくいくつかのメタモルフィズムにも適用で き,その柔軟性から並列計算によって実装することも可能である.

2日目午前の部 (3月5日 9:00-12:10)

9:00-10:00 セッション6 招待講演2 (座長 勝股 審也 (京都大学))
高速SATソルバーの実装と理論
鍋島 英知 (山梨大学)
概要  命題論理式の充足可能性判定問題(SAT)は,計算機科学における最も基本的で本 質的な組合せ問題である.90年代末頃からSAT問題を解くソルバーの性能は飛躍 的に向上しており,数百万の名大変数からなる大規模な問題を解くことが可能 になってきている.この性能向上をうけて,SATはシステム検証やプランニング, スケジューリング,制約充足問題などの分野に応用され,近年急速に発展を続 けている.本発表では,高速SATソルバーの代表的な要素技術と最新動向,開発 の苦労話について紹介する.
10:00-10:10 休憩
10:10-10:55 セッション7 論理の応用 (座長 中澤 巧爾 (京都大学))
SAT符号化を用いたパッキング配列の構成 [C1]
則武 治樹(1), 番原 睦則(2), 宋 剛秀(2), 田村 直之(2), 井上 克巳(3) ((1)神戸大学大学院システム情報学研究科 (2)神戸大学情報基盤センター (3)国立情報学研究所情報学プリンシプル研究系)
概要  近年,大規模な命題論理の充足可能性判定(SAT) 問題を高速に解くことが可能 なSAT ソルバーが実現され,制約充足問題(CSP; Constraint Satisfaction Problem) を SAT 問題に符号化して,高速なSAT ソルバーを用いて求解するSAT 符号化の研究が注 目を集めている.パッキング配列(PA; Packing Arrays) の構成は,組合せデザイン分野 の問題の1 つである.PA は別名で相互直交的な部分ラテン方陣系とも呼ばれる困難な 組合せ問題であり,データベースのディスク最適配置などへの応用が知られている.本 論文では,SAT 符号化を用いてPA を構成する問題を解く手法について述べる.提案 手法は簡潔な制約モデル,順序符号化法,SAT ソルバーの効果的な組合せに基づいてい る.まず最初に,PA を構成する問題に対して4 つの制約モデルを提案する.次に,こ れらの制約モデルを順序符号化法を用いてSAT 問題に符号化する方法を示す.なかで も,基本・相違モデルは,与えられたPA のパッキング制約について,符号化後の節数 を小さく抑えられる点が特長である.最後に,組合せデザイン・ハンドブックにある最 大のPA を構成する問題(全46 問) を用いて実行実験を行った結果,提案手法は最適値 が未知であった2 問について既知の上限が最適値であることを示し,さらに,5 問につ いて新しい下限を得ることに成功した.
A Data-flow Network That Represents First-order Logic for Inference [C2]
Hideaki Suzuki(1), Mikio Yoshida(2), Hidefumi Sawai(1) ((1)(独)情報通信研究機構 (2)株式会社ビービーアール)
出典: TAAI(Conference on Technologies and Applications of Artificial Intelligence) International Track 2012.11.16-18 Tainan, Taiwan http://idb.csie.ncku.edu.tw/taai2012conference/ (掲載済)
10:55-11:05 休憩
11:05-12:10 セッション8 検証 (座長 青木 利晃 (北陸先端科学技術大学院大学))
JNI規則違反検出ツールSEANを用いたAndroidのバグ修正 [C1]
西脇 春名(1), 鵜川 始陽(2), 馬谷 誠二(1), 八杉 昌宏(3), 湯淺 太一(4) ((1)京都大学大学院情報学研究科 (2)電気通信大学大学院情報理工学研究科 (3)九州工業大学大学院情報工学研究院 (4)京都大学名誉教授)
概要  Java Native Interface (JNI) を用いてネイティブコードを書く場合,C++言語な どのコンパイラがチェックできない特有の規則が存在する.特に,Android バージョン 2.3.7 のフレームワークもJNI の規則に違反しており,ビルド時の設定を変更すると,ブー トさえできなくなる.そこで本研究ではAndroid の規則違反を検出するために,Java オ ブジェクトへの参照の扱いについての規則違反に焦点を絞り,規則違反検出ツールSEAN を開発した.SEAN はJava オブジェクトへの局所参照を有効範囲外で使う規則違反の 可能性と,参照同士の比較に誤ってC++言語の比較演算子を用いる規則違反を検出する. SEAN で検出された規則違反を修正すると,ビルド時の設定を変更しても正しくブート するようになった.その過程で多くの偽陽性(false positive)が見受けられたため,特 定の関数を検出対象から除外できるようSEAN の改良も行った.
Reachability Analysis of the HTML5 Parser Specification and its Application to Compatibility Testing [C2]
Yasuhiko Minamide, Shunsuke Mori (University of Tsukuba)
出典: Proc. the 18th International Symposium on Formal Methods LNCS 7436, pp. 293-307, 2012 (掲載済)
Automating Relatively Complete Verification of Higher-Order Functional Programs [C2]
Hiroshi Unno(1), Tachio Terauchi(2), Naoki Kobayashi(3) ((1)University of Tsukuba (2)Nagoya University (3)University of Tokyo)
出典: In the Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013) (掲載済)

2日目午後の部 (3月5日 13:30-18:35)

13:30-14:45 セッション9 書き換え系 (座長 岩見 宗弘 (島根大学))
ボトムアップ書き換えに基づく最内書き換え到達可能性判定 [C1]
高橋 翔大, 青戸 等人, 外山 芳人 (東北大学電気通信研究所)
概要  ボトムアップ書き換えに基づく項書き換えシステムの到達可能性判定法がDurand ら(2007) によって提案されている.本研究では,ボトムアップ項書き換えシステムの クラス(BU) を最内書き換えに変更した最内ボトムアップ項書き換えシステムのクラス (IBU) を提案し,IBU に含まれる項書き換えシステムの最内書き換え到達可能性が判定 可能であることを示す.項書き換えシステムがIBU に属するか否かは一般には決定不能 である.そこで,IBU の部分クラスである強最内ボトムアップ項書き換えシステムのク ラス(SIBU) を提案し,項書き換えシステムがSIBU に属するか否かが決定可能である ことを示す.
書き換え帰納法に基づく帰納的定理の決定可能性 [C1]
中嶋 辰成, 青戸 等人, 外山 芳人 (東北大学電気通信研究所)
概要  等式論理において,自然数やリストなどのデータ構造上で成立する等式を帰納 的定理とよぶ.等式が帰納的定理であるか否かは一般的には決定不能であるが,いくつ かの部分クラスに対する決定手続きが知られている.Giesl ら(2001,2003) の行なった被 覆集合帰納法に基づく決定手続きをもとに,Falke ら(2006) は書き換え帰納法に基づく 決定手続きを提案した.また,外山(2002) は,書き換え帰納法に基づき帰納的定理の判 定問題を抽象的なリダクションシステムの等価性判定問題としてとらえることで,等式 が帰納的定理であるか否かを決定可能にする十分条件を示した.しかし,両者が保証し ている決定可能な帰納的定理のクラス間には包含関係がない.そこで,本論文ではFalke らの手法をもとに外山の結果を拡張することで,従来よりも広い決定可能な帰納的定理 のクラスを示す.
静的依存対法 -再帰定義は定義か?- [C1]
草刈 圭一朗 (名古屋大学大学院情報科学研究科)
概要  関数プログラミング言語を用いてプログラミングする際には停止性を保証する ために,多くのプログラマーは関数の再帰定義を行う際に引数の重みが減少するように プログラミングする.逆に言うと,再帰構造を適切に設計することにより停止性が保証 されるという常識が存在する.しかし,この常識が成立しない例が存在する.我々は静 的な再帰構造解析に基づく停止性証明法である静的依存対法を関数プログラムの計算モ デルである書換え系上で与え,上述の常識の成立を保証する具体的な条件を与えた.こ の成果の鍵は,型付きλ計算の停止性証明のために導入された強計算性の概念に基づく 再帰構造という非常に抽象的な概念の定式化に成功したことにある.その後も,静的依 存対法を実用的な関数プログラミング言語に対応させるべくML 多相型や直積型や代数 データ型を含む書換え系に拡張していった.本論文では,関数プログラミング言語で広 く利用されているパターン付きλ式を含む体系上に静的依存対法を拡張する.
14:45-15:00 休憩
15:00-16:10 セッション10 関数型言語2 (座長 番原 睦則 (神戸大学))
SML#のデータベース連携機能を活用したウェブアプリケーション構築技術 [C1]
藤井 貴啓(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院情報科学研究科 (2)東北大学電気通信研究所)
概要  ウェブアプリケーション開発環境の重要な役割の1 つは,ウェブアプリケーションに とって必須のデータベース機能の統合と考えられる.もし,データベース機能が統合さ れたプログラミング言語があれば,既存のウェブアプリケーションフレームワークと同 様の高水準でかつより堅牢で拡張性に富むウェブアプリケーション開発環境を,プログ ラミング言語環境として提供できると期待される.本研究では,この洞察に基づき,デー タベース機能をML 系高水準言語にシームレスに統合したSML# 言語を用いて,データ モデルの異なる2 つのウェブアプリケーションの試作を行い,データベース機能を統合 したML 系関数型言語によるウェブアプリケーション開発の可能性を検討した.両試作 とも,データベースの連携等の高度な機能により,比較的容易に開発を行うことができ た.この結果は,我々が予期した高い生産性を十分に期待されるものである.
コンパイラの型推論を利用した型スライス作成手法の提案 [C1]
対馬 かなえ, 浅井 健一 (お茶の水女子大学)
概要  本論文では,コンパイラに備わっている型推論器をそのまま使い,型エラース ライスを作成する手法について述べる.型エラースライスとは型エラーのあるプログラ ムのうち,型エラーに関係がある箇所のみを抽出したプログラムである.型スライサー が実装できれば,我々の先行研究の型デバッガにスライスを導入することで動作を改良 出来る. 本論文では,コンパイラの型推論器を使用して,二段階の操作で型エラースライスを 求める手法を提案する.まず一段階目としては,型エラーのあるプログラムの一部を型 制約を持たない式に置き換え,コンパイラの型推論器にかけて型エラーか否かを判別す ることで,連結した型エラースライスを求める.二段階目としては,一段階目で求めた 型エラースライスに対して一部を型制約を持たないが部分項を持つような式に置き換え, 一段階目と同様にコンパイラの型推論器にかけることで,より小さい型エラースライス を求める. 詳細には,let 多相を持つプログラムを対象として提案手法を説明する.型エラースラ イスの性質として極小性および局所性を定義し,それらを満たすスライスを求める手法 について述べる.また,その手法をOCaml の型推論器を用いて実装した型スライサー と,それから得られたスライスをどのようにデバッグで使用するかについて述べる.
Path resolution for recursive nested modules [C2]
Jacques Garrigue(1), 中田 景子(2) ((1)名古屋大学 (2)タリン工科大学)
出典: Higher-Order and Symbolic Computation (2012) 24:207-237 http://link.springer.com/article/10.1007%2Fs10990-012-9083-6 (掲載済)
16:10-16:25 休憩
16:25-17:10 セッション11 言語の設計と実装 (座長 青谷 知幸 (北陸先端科学技術大学院大学))
JavaScript 仮想機械におけるQuickeningの効果 [C1]
高田 祥(1), 鵜川 始陽(1), 中野 圭介(2), 岩崎 英哉(1) ((1)電気通信大学大学院情報理工学研究科 (2)電気通信大学先端領域教育研究センター)
概要  JavaScript はプログラムを実行するまで変数の型が決まらず,プログラムの実 行中に変数の型が変わることがあるので,実行時情報を利用した最適化が効果的であ る.このような最適化のひとつにQuickening がある.Quickening とは,プログラム中 の仮想機械命令をプログラム実行中に別の命令に書き換えることにより,実行時性能を 上げようという手法である.本論文は,JavaScirpt 仮想機械において,グローバル変数 へのアクセスを行う命令,オペランドの型によって処理が分岐する命令の両者に対して Quickening を適用し,実験を通してその効果を議論する.実験結果から,行列乗算,シ フト演算を行うマクロベンチマークにおいて,速度向上が確認できた.
Method Slots: Supporting Methods, Events, and Advices by a Single Language Construct [C2]
YungYu Zhuang, Shigeru Chiba (The University of Tokyo)
出典: Aspect-Oriented Software Development (AOSD) 2013 (掲載予定)
17:10-17:20 休憩
17:20-18:35 セッション12 プログラム変換 (座長 松崎 公紀 (高知工科大学))
二次元最大重み和問題のプログラム変換に基づく解法 [C1]
小石 真人(1), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院情報科学研究科 (2)東北大学電気通信研究所)
概要  我々は二次元最大重み和問題に対するプログラム変換に基づく解法を提案する. 二次元最大重み和問題とは,データ中から抜き出された要素の組みについて,それらがあ る述語を満たしつつ,それらの重み和が最大になるような組み合わせを探し出す問題で ある.二次元最大重み和問題の一つとして捉えられる問題に,Fukuda ら(ACM TODS, 2001) の提案した,ある種の関係性をO(n^3) で求めるような数値属性間相関ルール抽出 がある.我々はそれらを含む問題一般に対して,プログラム変換の観点から捉えた解法 を与える.その導出には,Sasano ら(ACM ICFP, 2000) の最大重み和問題の線形時間 解法の導出法と,Liu ら(ACM TOPLAS, 2005) の提案したincrementalization を用い る.これにより得られたプログラムはある種のクラスに属する二次元最大重み和問題を O(n^3) で解く.
Scala 上のプログラム運算支援システム [C1]
高橋 一平(1), 岩崎 英哉(2) ((1)電気通信大学情報工学科 (2)電気通信大学大学院情報理工学研究科)
概要  プログラム運算とは,人にとって理解しやすいが必ずしも効率が良いとは限ら ないプログラムを,数学的に証明された変換規則を用いることによって,意味を変える ことなく効率の良いプログラムに変換する手法である.プログラム運算は有用であるが, 変換規則に関する知識や,場合によっては新たな関数や演算子の導入などが必要となる ため,手動で行うには手間がかかる.これまで,プログラム運算を支援するシステムも いくつか開発されているが,研究者向けであり,広く使われるには至っていない.本研 究は,近年利用者が増えつつあるプログラミング言語Scala を対象として,より実用性 の高いプログラム運算支援システムの構築を目指す.本システムは,メタプログラミン グを利用した構文木操作を用いて,ユーザと対話的にプログラムの運算を行う.さらに, 変換規則の記述のためのドメイン特化言語を提供する.これにより,運算システム本体 に変更を加えることなく,変換規則を追加することができる.
例外と限定継続命令をサポートする評価器からの仮想機械とコンパイラの導出 [C1]
増子 萌, 浅井 健一 (お茶の水女子大学)
概要  限定継続の命令shift/reset を用いると,ユーザによるプログラムの実行順序の制 御が可能となり,さまざまな応用例が考えられる。shift/reset の使用をサポートす るため,我々は先行研究においてCaml Light システムを変更し,shift/reset を直接 実装した。基本的にshift/reset はスタックフレームのコピーで実装出来るが,Caml Light は例外処理をサポートするために例外用ポインタを利用しているので,単純なフ レームのコピーでは実装出来ず,その正当性は保証されていなかった。すでに先行研究 でλ計算をshift/reset で拡張した言語のインタプリタから仮想機械とコンパイラが 導出されているため,本研究ではこれを例外で拡張し,例外も含めた実装に正しさを保 証しやすい形で仮想機械とコンパイラを導出した。

2日目夜の部 (3月5日 20:30-22:00)

20:30-22:00 セッション13 ポスター・デモ2
CoqによるOpenFlowネットワークの形式化とFlowVisorの検証 [C3 (ポスター)]
逸見 港(1), 田辺 良則(2), 萩谷 昌己(1) ((1)東京大学 (2)国立情報学研究所)
概要 OpenFlowは近年めざましく発展しているSDN(Software Defined Network)技術であり、OpenFlowネットワーク上で動くさまざまなアプリケーションが開発されている。特にFlowVisorはその一つであり、ユーザにスライスと呼ばれる仮想ネットワークを提供する。ユーザは同じ実ネットワークを利用しながら、他のユーザやFlowVisorの存在を気にせず自分の仮想ネットワークのテストができる。しかしOpenFlowネットワークの局所性と柔軟性ゆえに、FlowVisorの仮想化の正当性は明らかでない。まずOpenFlowネットワークの形式的モデルを与えたあと、ユーザの意図したネットワークとFlowVisorにより割り当てられたスライスが同じ動作をすることを定理証明器Coqを用いて証明する。
Towards Bidirectional Graph Transformations with High-Level Patterns [C3 (ポスター)]
Tao Zan(1), Soichiro Hidaka(2), Hiroyuki Kato(2), Zhenjiang Hu(2) ((1)The Graduate University for Advanced Studies (2)National Institute of Informatics)
概要 Bidirectional graph transformation provides a novel mechanism for synchronizing and maintaining the consistency of information between two related models, and it has many potential applications in model driven development. Recently a powerful tool called GRoundTram has been developed to enable compositional development of well-behaved and e cient bidirectional graph transformations. However, graphs in GRoundTram are low-level edge-labeled graphs, being much di erent from real-world graphs, which usually have more sophisticated representations. In this paper, we propose BiQuery, a bidirectional graph transformation language for GRoundTram that supports using user-friendly(high-level) graph patterns to manipulate real-world graphs directly. Specically, we provide users with a general way of defining the schema of a real-world graph and of constructing a graph instance that conforms to the schema. We then let users write forward transformations in BiQuery directly over the general representation of graphs using high-level graph patterns, and achieve backward transformations for free by automatically translating BiQuery to UnQL+ which is the bidirectional graph transformation language in GRoundTram. We have implemented this translation using Haskell, and tested the system with many nontrivial examples including the known bidirectional transformation between UML classes and relational DBs.
最大流を扱うプログラムに対する最悪テストケース生成 [C3 (ポスター)]
山口 洋 (東京大学)
概要 ACM-ICPC を始めとするプログラミングコンテストにおいては、最も計算時間が長くなると見込まれるテストケースを用意することが必要である。しかしながら、最大流を題材にする場合、探索順序によって計算時間が大きく変化してしまうため、最悪テストケースとして十分機能するものを用意することが困難であった。そこで本研究では枝の順序のみに注目し、計算時間が最長となるように枝の順序を並び替えたテストケースを、実装に応じて個別に生成することを目指す。その方法として、ソートにおける稲葉のアプローチを元にした貪欲法と、 Java PathFinder を用いた全探索を試した結果について述べる。
決まった文法を持たないプログラミング言語の実現に向けて [C3 (ポスター)]
市川 和央, 千葉 滋 (東京工業大学 情報理工学研究科 数理・計算科学専攻)
概要 本発表ではユーザ定義演算子による決まった文法を持たないプログラミング言語の実現に関する研究の経過を述べる。我々はこれまでの研究で、静的型付け言語上に解析表現文法(PEG)と同等の表現力を持つユーザ定義演算子が導入できることを明らかにした。このユーザ定義演算子に環境を操作するメタ演算を加えることで、プログラミング言語全体を表現することが可能となることが予想される。言語全体が演算子で表現できれば、プログラマは場面に応じて最適な文法を選んで開発を行うことができるため、プログラムの可読性や保守性、生産性 が向上する。本発表ではそのような演算子の設計に関する議論を行いたいと考えている。
アノテーションをもとにオブジェクトのデータレイアウトを自動的に変えるJavaコンパイラ [C3 (ポスター)]
汐田 徹也, 山口 洋, 千葉 滋 (東京大学情報理工学系研究科創造情報学専攻)
概要 本研究では,アノテーションをもとにオブジェクトのデータレイアウトを自動的に変えるJavaコンパイラを提案する.これは,ユーザが定義したデータレイアウトを変換し,プログラムの性能の向上を図るものであり,ユーザが理解しやすいレイアウトと性能が向上するレイアウトの設計が異なる場合に,それらを両立させることができる.我々は,予備実験によって,Javaにおいてもそのようなコンパイラが有用であることを実証しており,現在,ガベージコレクタへの対応などを検討しながらコンパイラの実装を進めている.
文脈移動法に基づく項書き換えシステムの自動変換 [C3 (ポスター・デモ)]
佐藤 洸一, 菊池 健太郎, 青戸 等人, 外山 芳人 (東北大学)
概要 プログラム変換は一般的に効率化を目的としており,プログラム検証や人間による理解を容易にすることを目的とした変換手法の研究は少ない.後者を目的とした変換手法のひとつとして,Giesl(2000)により提案された文脈移動法が知られている.これは,適当な条件のもとで,効率的な末尾再帰形プログラムから自動検証に適した単純再帰形プログラムへの等価変換を行う手法である.本報告では,文脈移動法に基づく項書き換えシステムの自動変換手法を提案するとともに,計算機上での自動変換実験について紹介する.
Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール [C3 (ポスター)]
宋 剛秀, 田村 直之, 番原 睦則 (神戸大学 情報基盤センター)
概要 Scarab は著者らが開発した Scala 上の制約プログラミング用 DSL であるCopris と同様のツールである.しかし Scarab では,SAT ソルバー以外の部分は,SAT 符号化の部分を含めてすべて Scala でコンパクトに記述されておりカスタマイズが容易であるという特徴を持つ.また SAT ソルバーとして利用している Sat4j に対する API を使用することにより,インクリメンタル SAT解法など最新の SAT 解法技術を実現できる.
束縛変数を考慮した名目書き換えシステムの実現法 [C3 (ポスター・デモ)]
鈴木 貴樹, 菊池 健太郎, 青戸 等人, 外山 芳人 (東北大学)
概要 束縛変数を簡潔に取り扱う枠組みとして名目項がUrbanら(2004)によって提案され,その枠組みに基づいた名目書き換えシステムの研究も進められている.しかし,これらの名目書き換えシステムは,書き換えステップの定義が簡明とはいえず,その実装法も必ずしも明確ではない.本報告では,書き換えステップごとにフレッシュなアトムを導入することで,より実装に適した名目書き換えシステムを提案するとともに,その実装について報告する.さらに,アトムの出現条件で拘束されている項の書き換えにおける提案システムの問題点について考察する.
依存型意味論による前提理論の形式化 [C3 (ポスター)]
石下 裕里, 戸次 大介 (お茶の水女子大学大学院 人間文化創成科学研究科 理学専攻 情報科学コース)
概要 前提とは形式意味論で長年議論されてきた現象の一つである。前提の分析はモデル理論的意味論に基づくものが主流であるが、この手法は計算機で扱うには不向きである。一方、証明論的手法を用いた分析にはMartin-Löf型理論やIllative Combinatory Logicに基づくものがある。しかしこれらの分析は前提現象しか分析できず、複数の言語現象を同時に取扱可能な統一的分析が求められている。そこで既に照応現象を証明論的に説明している依存型意味論(DTS)を採用する。DTSの特徴として動的であることが挙げられる。動的意味論と前提の繋がりは指摘されているが、DTSでは前提の記述形式は与えられていない。そこで本研究ではDTSの枠組みによる前提理論の確立を試み、その理論によって前提の性質が証明論的に説明されることを示す。
多段階計算の体系 $\lambda^\triangleright$ への持ち上げ操作の導入 [C3 (ポスター)]
花田 裕一朗, 五十嵐 淳 (京都大学工学部 京都大学大学院情報学研究科)
概要 多段階プログラミングとは実行時にプログラムコードの生成や実行を許すようなプログラミング技法であり,MetaOCaml などいくつかの多段階プログラミング言語が提案・実装されている.多段階プログラミングを形式化した体系として Tsukada と Igarashi により $\lambda^\triangleright$ が提案されている.この体系では、型検査によって, 実行時に生成したプログラムも安全に実行できることが保証される. しかし, この体系では,持ち上げや CSP と呼ばれる,計算した値を次の段階の計算を行うコードの中へと埋め込む機能がモデル化されていない.本研究では,$\lambda^\triangleright$ に持ち上げ操作を導入し,その型システムの健全性を証明した.
ドメイン特化言語処理系実装支援ライブラリのメタプログラミングによる実装 [C3 (ポスター・デモ)]
塩田 雅人, 岩崎 英哉 (電気通信大学大学院情報理工学研究科)
概要 ドメイン特化言語はCやJava等の汎用言語と比べ,その特定用途において生産性や品質を向上させる.ドメイン特化言語の処理系を実装するための従来の手法では,Yacc 等で生成した構文解析器を用いて抽象構文木を生成し,それを解釈実行したり,あるいはさらに中間コードに変換して実行することが多い.しかしこの手法では,処理系の構築の前にYacc等による処理があるのに加え,処理系の拡張を簡単に行うこともできない.本研究ではD言語のメタプログラミングによって構文解析器と仮想マシンをそれぞれ生成する.メタプログラミングで実装することで,処理系の構築はコンパイラのみで行え,拡張も自然に行うことが可能となる.
Implementing Wormholes with Commutative Causal Arrows and Type-level programming [C3 (ポスター)]
Raphael Gaschignard (Department of Creative Informatics, Graduate School of Information Science and Technology, University of Tokyo )
概要  In the Arrowized variant of Functional Reactive Programming popularised by Yampa, two attempts have been made to make a system that allows to verify at compile-time whether resources are properly accessed. These attempts, named wormholes by their author, also allow for a new style of writing AFRP-style code, that allow for greater modularity.However, these implementations either place too many usage restrictions, invalidating many useful programs, or have an incomplete implementation. This proposal offers a complete implementation, with slightly different semantics than the previous attempts to allow for more use cases. This implementation makes heavy use of type-level programming to do its usage verifications. It has equivalent semantics to commutative causal arrows, which allow us to implement a normalisation optimisation described in a previous research paper.
Neighborhood-sheafによる一階述語条件論理の意味論 [C3 (ポスター)]
山本 華子, 戸次 大介 (お茶の水女子大学大学院人間文化創成科学研究科)
概要 Neighborhood-sheaf semantics (NSS)は、 一階述語様相論理の意味論の一種であり、 領域を可能世界の集合上の層として捉えることによって定義されたものである[Kishida 2011]。 これは 同様に構成されたKripke-sheaf とtopological-sheaf の意味論の一般化であり、定義の自由度が高い。本研究では、一階述語様相論理の一種で暗黙の前提を扱う、一階述語条件論理[Priest 2008]のNSSを与えることを試みる。
Product lines implemented in feature-oriented programming are not sometimes object-oriented [C3 (ポスター)]
武山 文信 (東京工業大学 情報理工学研究科 数理・計算科学専攻)
概要 機能指向プログラミング (FOP) は、ある機能のためのコードを1つのモジュールに記述するプログラミングパラダイムである。多くの FOP 言語はオブジェクト指向プログラミング (OOP) に、横断的関心事を分離する機構を加えることで実現されている。しかしながら、実際に FOP で実装されたコードを調べてみると、クラスの継承など OOP の実装手法を十分に使用していないコードが見つかり、コードクローンやクラスの肥大化などの問題が起きている。本ポスターではこの問題の例を紹介し、FOP のコード品質を測る方法について議論したい。
ヘッダーファイルからSML#へのC関数の自動インポート [C3 (ポスター・デモ)]
相澤 遥也(1), 徳田 亮平(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学工学部 (2)東北大学電気通信研究所)
概要 SML#にはC言語の関数を扱うためのインポート機能がある。インポートするには、使用する関数それぞれについて関数名と対応する型を記述する必要があり、人の手で大量の関数を導入するのは労力を要する。そこでC言語で用いられるヘッダーファイルから、機械的にインポートに必要なコードを生成する機能を作成した。この生成器により、c言語のヘッダーファイルを入力することで、そのヘッダーファイル内の関数をSML#で容易に使用することができる。
Towards a MapReduce implementation for distributed query evaluation on labeled graph [C3 (ポスター)]
Andres Pardo(1), Le Duc Tung(2), Zhenjiang Hu(3) ((1)UPC-BarcelonaTech (2)The Graduate University for Advanced Studies (3)National Institute of Informatics)
概要 In this poster, we present a Scala implementation of a query evaluator on semistructured data modeled as a rooted, labeled and distributed graph. This implementation is based on the theoretical model contributed by Dan Suciu. He showed evaluation algorithms in which the efficiency definition bounds the number of communications to a constant, and the amount of data transferred is related to the size of the query's answer and the total number of links between the distributed database. That definition fits well with the MapReduce paradigm where the computation is divided into two phases and between them there is a huge data shuffle in a single communication step. In the proposed system, the servers have a separate part of the database and the client sends the query to them. First, each server computes a partial result, a local accessibility graph and sends the local accessibility graph to the client, then the client combines them to create a global one and broadcast this information back to the servers, where they use it to compute a final local answer based on the partial result. By concatenating these answers the client fulfills the original query. The current implementation is tested on a sequential manner versus real world data extracted from Twitter, as a first step towards a future MapReduce implementation.
Extending event-driven programming to support reactive programming by adding an inference mechanism [C3 (ポスター)]
莊 永裕 (東京大学 大学院 情報理工学系研究科 創造情報学専攻 千葉滋研究室)
概要 With reactive programming data flows can be expressed easily and the changes are propagated implicitly. For example, in a spreadsheet program we can assign "=B1+C1" to the cell A1 then it is updated automatically whenever the cell B1 or the cell C1 is modified. Functional reactive programming (FRP) successfully brought reactive programming to programming languages by introducing behaviors and events. However, current approaches are either far from object-oriented programming or heavily dependent on the libraries made for behaviors. To make reactive programming more compatible with object-oriented programming, we analyzed the essentials of reactive programming and found the difference from event-driven programming. Event-driven programming can be used to express the same logic in reactive programming, but programmers have to create events for fields and explicitly bind the handlers to all related events by themselves. We introduce a new operator for method slots to support reactive programming by proposing a way to find out events by inference and bind the handler to them implicitly. We also try to implement a typical usage in spreadsheet programs, "A1=B1+C1", by our proposal and a FRP language respectively, to show the similarity between them.
CoqにおけるMonads with Predicate Liftingsの実装と考察 [C3 (ポスター)]
須田 啓司 (千葉大学大学院 理学研究科)
概要 Coqでは,Haskellと同様に型クラスという形でモナドを用い,計算効果を伴うプログラムを記述する為の枠組みが得られる.しかし,モナドを用いて記述されたプログラムに関する推論は,その具体的な実装が与えられないと行えない.本研究は,モナドを用いて記述されたプログラムについての推論を統一的に扱う為の枠組みを構築することを目指すものであり,枠組みの基盤としてJacobsによるMonads with Predicate Liftingsを利用することを試みる.本発表では,その実装と,計算効果との関連や推論への応用についての考察を行う.
JavaCat: Realizing Context as Fluent [C3 (ポスター)]
紙名 哲生(1), 青谷 知幸(2), 増原 英彦(1) ((1)東京大学 (2)北陸先端科学技術大学院大学)
概要 これまで数多くの文脈指向プログラミング(COP)言語が提案され,それぞれ文脈とそれに依存する振舞の実行時切り替え機構が独自に提案されてきた.しかしそれらの優位性はプログラム対象によって異なる.またこれら全ての言語機構を提供するような言語は存在しないし,実現したとしても非常に複雑な言語となる.また,既存の言語には,1.条件の真偽に基づいて文脈を活性化する機構,2.文脈や振舞の活性化の記述をモジュラーに拡張する機構が存在しない.本発表では,既存の機構を包含し,且つ上記1.や2.を実現する新たなCOP言語機構として,fluentと暗黙的層活性を提案し,それらを実現する言語JavaCatを提案する.
Rubyの操作的意味論の形式的定義に向けて [C3 (ポスター)]
深澤 優鷹(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院 情報科学研究科 (2)東北大学 電気通信研究所)
概要 この研究ではRubyの形式的な定義を目的とする.Rubyの仕様は現在自然言語と実装によって与えられている.我々はRubyの形式的な理解のために,仕様と実装の分析を行った.この分析によると理解のための最大の難関はイテレータである.この課題を克服するために我々はRubyインタプリタの実装からイテレータの本質を抽出することを試みた.
オブジェクト指向計算体系プロダクトラインの合併型による拡張 [C3 (ポスター)]
奥村 健太郎, 五十嵐 淳 (京都大学大学院 情報学研究科)
概要 証明支援系における証明の再利用を目的として,Delawareらによって形式定理プロダクトラインと呼ばれる手法が提案された,この手法は,型無・型付ラムダ計算の項など,定義が似通った帰納的集合についての性質の証明を対象にしており,共通部分となるモジュールと差分を記述したモジュールを結合することによって,定義や証明を構築する.Delawareらは提案手法を用いて,CoqでFJとその拡張体系を形式化した.本研究ではDelawareらが想定していなかったと考えられる合併型による拡張の形式化を通じて,Delawareの手法の追試を行った.
SML#のSQL統合へのgroup byの導入 [C3 (ポスター)]
斎藤 皓(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院 情報科学研究科 (2)東北大学 電気通信研究所)
概要 SML#はSQLをシームレスに統合している.しかし,現在のSML#はすべてのSQL構文をサポートしていない.より完全なSQLのサポートを目指し,本研究ではその第一歩としてgroup by及び集約関数に注目する.SML#のSQL統合はSQLの各構文要素に対する型つきラムダ式への翻訳によって実現されている.この方針にしたがって,group by及び集約関数に関する型付けと操作的意味を検討した.
不定元入り文字列を扱う言語XPCFの表現能力 [C3 (ポスター)]
寺山 慧, 立木 秀樹 (京都大学人間・環境学研究科)
概要 関数型言語PCFを拡張することで, 不定元を高々一つ含む無限文字列を扱える言語XPCFを定義できる. XPCFの表示的意味は, ドメインとその上の連続関数として与えられるが, 全ての計算可能な要素がXPCFの項で表示できるわけではない. 本発表では, まず, XPCFはparallel ifを書けることを示す. さらに, XPCFの項をPCF+pifの項に変換することによって, モデル上の全ての有限な要素がXPCFの項として表示できるが, 連続な関数であるexistential quantifierをXPCFで書けないことを示す. しかし, XPCFにexistential quantifierを加えることによって, 普遍性, すなわちモデルの全ての計算可能な要素がXPCFで表示できることを証明する.
正規言語の列挙: プログラミングへの応用 [C3 (ポスター・デモ)]
新屋 良磨 (東京工業大学大学院情報理工学研究科数理・計算科学科専攻佐々研究室)
概要 正規言語(正規表現)は文字列検索のための便利なツールとしてプログラマーに深く愛されている. 一方,正規言語の検索以外への応用は一般のプログラマーにとって知られていないモノが多い. その一つとして,正規言語の列挙があり,これは任意の正規言語に対してn番目の文字列を計算する というシンプルなモノである.本発表では正規言語の列挙のいくつかの応用を,著者によるオープン ソース・ソフトウェア RANS を用いて紹介する.

3日目午前の部 (3月6日 9:00-13:00)

9:00-10:30 セッション14 意味論 (座長 角谷 良彦 (東京大学))
Structural Recursion for Querying Ordered Graphs [C1]
Soichiro Hidaka(1), Kazuyuki Asada(1), Zhenjiang Hu(1), Hiroyuki Kato(1), Keisuke Nakano(2) ((1)National Institute of Informatics (2)University of Electro-Communications)
概要  Structural recursion, such as fold on lists or catamorphism on algebraic data structures including trees, plays an important role in functional programming, providing a systematic way for construction and manipulation of functional programs. It is, however, a challenge to define structural recursions for graph data structures, the most ubiquitous data in computing. This is because unlike lists and trees, graphs are essentially not inductive and cannot be formalized as an initial algebra in general. In this paper, we borrow from database community the idea of structural recursion on how to restrict recursion suitably for infinite unordered regular trees so that the recursion for finite graphs preserves finiteness of graphs and become terminating, which are desirable properties for query languages. We propose a new graph transformation language \lambda_{FG} for transforming and querying ordered graphs, based on well-defined bisimulation relation on ordered graphs with special \epsilon-edges. The language \lambda_{FG} is a higher order graph transformation language, extending the simply typed lambda calculus with graph constructors and more powerful structural recursions, which is extended for transformations in sibling dimension. It not only gives a general framework for graph manipulation and reasoning, but also shows a solution to the open problem of how to define a structural recursion on ordered graphs, with the help of proposed bisimilarity for ordered graphs with \epsilon-edges.
shift/reset 付きTDPEの抽出 [C1]
廣田 知子, 浅井 健一 (お茶の水女子大学)
概要  Danvy により提案されたtype-directed partial evaluator (TDPE) は,与えら れた項をnormal form に評価する関数であり,Filinski によってcall-by-value 及びcall- by-name の単純型付きλ計算におけるTDPE の正当性が示されている.一方,対馬ら の論文によって,shift/reset 付きに拡張されたTDPE が提案されているが,未だ正当性 は保証されていない. 本研究では,対馬らによって提案されたTDPEを参考に,CPS 変換を行ったshift/reset 付きTDPE を定義し,その正当性を示す試みを行った.証明はCPS 変換した論理述語を 用いて行った.さらに,call-by-value のshift/reset を含んだ型付きλ 計算の正当性(本 研究で定義した論理述語の定義を満たす)の証明を定理証明系システムCoq によって定 式化することにより,OCaml 言語のプログラムを抽出した.抽出されたプログラムは, 複雑にはなっているものの,概ね対馬らによって提案されたshift/reset 付TDPE の形 を成していることが見て取れるような構造になっている.
Hyperstream Processing Systems --- Nonstandard Modeling of Continuous-Time Signals [C2]
Kohei Suenaga(1), Hiroyoshi Sekine(2), Ichiro Hasuo(2) ((1)Kyoto University (2)Univerisity of Tokyo)
出典: POPL 2013: 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Rome, Italy, January 23-25, 2013 (掲載済)
Polymorphic Abstract Syntax via Grothendieck Construction [C2]
Makoto Hamana (群馬大学工学研究科情報工学専攻)
出典: 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2011), Lecture Notes in Computer Science 6604, p.381-395, Springer-Verlag, 2011 (掲載済)
10:30-10:45 休憩
10:45-12:15 セッション15 通信と並行計算 (座長 蓮尾 一郎 (東京大学))
対応表明つきプロトコル記述からSpiCAへの複数セッションを考慮した変換 [C1]
佐藤 悠史, 住井 英二郎 (東北大学大学院情報科学研究科)
概要  セキュリティプロトコルはしばしば、ナレーションと呼ばれる非形式的な記法 を用いて定義される。住井らはナレーション記法から、セキュリティプロトコルの形式 的記述の枠組みである、Abadi とGordon のspi 計算への変換を定義した。本研究では、 住井らの変換をWoo とLam の対応表明で拡張する。対応表明とは、プロトコルにおけ るメッセージの真正性を定式化するための表明である。本研究ではナレーション記法を 対応表明で拡張し、小林らのSpiCA(spi 計算を対応表明で拡張した体系、および、そ の体系において真正性を検証するための型システム)への変換を定義する。特に、住井 らが考慮していなかった複数セッションの並行実行を考慮する。具体的には以下のよう に変換を定義する。(1) プロトコルの参加者と役割を分け、全ての参加者が全ての役割 を行う。また、共有鍵の対称性を反映する。(2) 攻撃者も参加者に含まれ、攻撃者の鍵 は公開される。
Automated Proof of Equivalence on Quantum Cryptographic Protocols [C1]
Takahiro Kubota(1), Yoshihiko Kakutani(1), Go Kato(2), Yasuhito Kawano(2), Hideki Sakurada(2) ((1)Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo (2)NTT Communication Science Laboratories, NTT Corporation)
概要  We present a software tool to prove behavioural equivalence of quantum processes and its application to Shor and Preskill's security proof of BB84 quantum key distribution protocol. It is recognized that security proofs of cryptographic protocols tend to be complex and hard to verify. The use of formal methods is a way to tame such complexity. To model quantum protocols, quantum process calculi have been used. For instance, we applied qCCS to Shor and Preskill's security proof in our previous work. Bisimulation is a key notion in process calculi that denotes two processes behave indistinguishably from the outside. However, by-hand verification of bisimilarity is often very tedious especially when transitions are long. We implemented a software tool to prove bisimulation of qCCS configurations, which are pairs of a process and an environmental quantum state. If the prover returns true with two input configurations, then they are bisimilar in qCCS. We applied the prover to Shor and Preskill's security proof, where BB84 is transformed to an equivalent secure protocol based on an Entanglement distillation protocol. We formalized BB84 and EDP-based protocol in our prover and automatically checked their bisimilarity.
Type-Based Safe Resource Deallocation for Shared-Memory Concurrency [C2]
Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi (Kyoto University)
出典: The Third Annual SPLASH Conference, OOPSLA Research Paper. Arizona, US. Oct. 19--26, 2012 (掲載済)
Session Types in Abelian Logic [C2]
平井 洋一 (東京大学大学院情報理工学系研究科)
出典: PLACES'13 (掲載予定)
12:15-12:25 本田耕平先生を偲んで
12:25-13:00 クロージング

注意: PPL2013 は国内の研究者に予備段階にある研究を発表する機会を与えるワーク ショップであるとともに,ここでの議論に基づき改良を加えた論文を国際会議 や学術雑誌に投稿することを推奨しています.そのため,ここにあるオンライ ン予稿集は(ISBN,ISSNなどを持たない)非公式のものであり,他の場所での出 版を妨げるものではありません.
本ページ上のカテゴリ1論文は各著者によって提供されたものであり,著作権 は各著者に属します.転載などに関しては各著作権者の許可を得る必要があり ます.
カテゴリ2は,査読付の国際会議または学術雑誌等で既発表(もしくは採録決 定済)であるが国内で未発表の研究を紹介をする場であり,そこでの発表は論 文の再出版・二重投稿などには該当しません.
NOTICE: PPL aims to function as an informal workshop series, which gives researchers an opportunity to disseminate their preliminary work and get feedback from the participants without precluding publication elsewhere. It encourages submissions of revised versions of the work to international conferences or refereed journals.
The second category of PPL ([C2] in the program above) is intended to help researchers disseminate their research to the domestic community by providing an opportunity to present their papers that have already been accepted by international conferences or journals (but not presented in Japan before). Therefore, presentations in this category, which are informal, should not be considered republication or results of double submissions of any kind.