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)東北大学電気通信研究所)
shift/reset によるモナドトランスフォーマの提案と実装 [C1]
金子 ちひろ, 浅井 健一 (お茶の水女子大学)
分割統治計算可能性の多相型を用いた保証 [C1]
森畑 明昌 (東北大学電気通信研究所)
15:05-15:20 休憩
15:20-16:20 セッション2 招待講演1 (座長 権藤 克彦 (東京工業大学))
数値計算のための大規模並列プログラムの自動生成
村主 崇行 (京都大学)
16:20-16:30 休憩
16:30-17:15 セッション3 遷移系と木変換器 (座長 中野 圭介 (電気通信大学))
Conditional Transformable Pushdown System: スタックの変換と検査が可能なプッシュダウンシステム [C1]
上里 友弥(1), 南出 靖彦(2) ((1)筑波大学情報学群情報科学類 (2)筑波大学システム情報系情報工学域)
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]
伊藤 宗平, 小林 直樹 (東京大学大学院情報理工学系研究科コンピュータ科学専攻)
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 (ポスター・デモ)]
坂口 和彦 (筑波大学 情報学群 情報科学類)
動的に変化するグラフのための効率的な一意エンコード生成手法 [C3 (ポスター)]
宮原 和大, 上田 和紀 (早稲田大学)
LMNtal処理系SLIMのマルチスレッド化による最短経路問題のデータ並列求解 [C3 (ポスター)]
青山 龍一, 上田 和紀 (早稲田大学)
SLIMの階層グラフのためのキャッシュコンシャスかつ効率的なデータ構造 [C3 (ポスター)]
吉田 健人, 上田 和紀 (早稲田大学)
線形純粋型理論 [C3 (ポスター)]
木村 大輔 (国立情報学研究所)
LMNtal並列モデル検査における状態生成数削減及び高速化 [C3 (ポスター)]
安田 竜, 上田 和紀 (早稲田大学)
Glasgow Haskell Compilerが提供するIOマネージャの並列化 [C3 (ポスター)]
山本 和彦 (株式会社IIJイノベーションインスティテュート)
型レベルプログラミングを用いたCoqからHaskellへのプログラム抽出 [C3 (ポスター・デモ)]
中村 宇佑 (東京大学情報理工学系研究科コンピュータ科学専攻(萩谷研))
Dialectica解釈と双方向変換とのCurry–Howard対応 [C3 (ポスター)]
浅田 和之 (国立情報学研究所)
JavaScript処理系に対する外部関数インタフェースの設計及び実装 [C3 (ポスター)]
谷村 明, 岩崎 英哉, 中野 圭介, 鵜川 始陽 (電気通信大学)
データフロー要約の構文主導型並列計算 [C3 (ポスター)]
佐藤 重幸(1), 森畑 明昌(2) ((1)電気通信大学 (2)東北大学電気通信研究所)
LMNtalコンパイラの検証に向けたグラフ書き換え操作の形式化 [C3 (ポスター)]
信夫 裕貴, 上田 和紀 (早稲田大学)
SIMT プログラムのためのホーア論理 [C3 (ポスター)]
小島 健介, 五十嵐 淳 (京都大学・JST CREST)
データベースを用いたMikiβの拡張に向けて [C3 (ポスター・デモ)]
中野 祥, 浅井 健一 (お茶の水女子大学)
適用する破壊的クラス拡張を実行時に切り替えるモジュールシステムMethod Shells [C3 (ポスター)]
竹下 若菜, 千葉 滋 (東京大学 情報理工学系研究科 創造情報学専攻)
HPCアプリケーション最適化に伴う計算漏れ検出手法の検討 [C3 (ポスター)]
穂積 俊平, 佐藤 芳樹, 千葉 滋 (東京大学大学院 情報理工学系研究科 創造情報学専攻)
メソッドのオーバーライドにより部分的実行順序が定義可能なHPC向け言語 [C3 (ポスター)]
宗 桜子, 佐藤 芳樹, 千葉 滋 (東京大学 情報理工学系研究科 創造情報学専攻 千葉研究室)
バックトラックによる正規表現マッチングの時間線形性判定 [C3 (ポスター)]
杉山 聡(1), 南出 靖彦(2) ((1)筑波大学 システム情報工学研究科 コンピュータサイエンス専攻 (2)筑波大学 システム情報系 情報工学域)
An Accumulative Computation Framework on MapReduce [C3 (ポスター)]
劉 雨(1), 江本 健斗(2), 松崎 公紀(3), 胡 振江(4) ((1)総合研究大学院大学複合科学研究科 (2)東京大学情報理工学系研究科 (3)高知工科大学情報学群 (4)国立情報学研究所アーキテクチャ科学研究系)
動的レイヤー合成のための型システム [C3 (ポスター)]
井上 裕昭(1), 五十嵐 淳(2), Robert Hirschfeld(3), 増原 英彦(4) ((1)京都大学工学部 (2)京都大学大学院情報学研究科 (3)Hasso-Plattner-Institut Potsdam (4)東京大学)
オーダー2の高階ブーリアンプログラムの文脈等価性に関する同値類列挙 [C3 (ポスター・デモ)]
長井 雅比古(1), 住井 英二郎(2) ((1)東北大学工学部情報知能システム総合学科 (2)東北大学大学院情報科学研究科)
高階再帰スキームのための交替性パリティ木オートマトンモデル検査器 [C3 (ポスター・デモ)]
藤間 幸一(1), 伊藤 宗平(2), 小林 直樹 (2) ((1)東京大学理学部情報科学科 (2)東京大学大学院情報理工学系研究科)
通信プロトコル仕様の形式化による形式検証とファジングテストへの応用 [C3 (ポスター・デモ)]
大岩 寛, Reynald Affeldt (AIST)
Metamorphism in Jigsaw [C3 (ポスター; C2から移動しました)]
中野 圭介 (電気通信大学 先端領域教育研究センター)
出典: Journal of Functional Programming (Cambridge University Press) (後日掲載予定 オンラインでは掲載済)

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

9:00-10:00 セッション6 招待講演2 (座長 勝股 審也 (京都大学))
高速SATソルバーの実装と理論
鍋島 英知 (山梨大学)
10:00-10:10 休憩
10:10-10:55 セッション7 論理の応用 (座長 中澤 巧爾 (京都大学))
SAT符号化を用いたパッキング配列の構成 [C1]
則武 治樹(1), 番原 睦則(2), 宋 剛秀(2), 田村 直之(2), 井上 克巳(3) ((1)神戸大学大学院システム情報学研究科 (2)神戸大学情報基盤センター (3)国立情報学研究所情報学プリンシプル研究系)
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)京都大学名誉教授)
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]
高橋 翔大, 青戸 等人, 外山 芳人 (東北大学電気通信研究所)
書き換え帰納法に基づく帰納的定理の決定可能性 [C1]
中嶋 辰成, 青戸 等人, 外山 芳人 (東北大学電気通信研究所)
静的依存対法 -再帰定義は定義か?- [C1]
草刈 圭一朗 (名古屋大学大学院情報科学研究科)
14:45-15:00 休憩
15:00-16:10 セッション10 関数型言語2 (座長 番原 睦則 (神戸大学))
SML#のデータベース連携機能を活用したウェブアプリケーション構築技術 [C1]
藤井 貴啓(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院情報科学研究科 (2)東北大学電気通信研究所)
コンパイラの型推論を利用した型スライス作成手法の提案 [C1]
対馬 かなえ, 浅井 健一 (お茶の水女子大学)
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)電気通信大学先端領域教育研究センター)
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)東北大学電気通信研究所)
Scala 上のプログラム運算支援システム [C1]
高橋 一平(1), 岩崎 英哉(2) ((1)電気通信大学情報工学科 (2)電気通信大学大学院情報理工学研究科)
例外と限定継続命令をサポートする評価器からの仮想機械とコンパイラの導出 [C1]
増子 萌, 浅井 健一 (お茶の水女子大学)

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

20:30-22:00 セッション13 ポスター・デモ2
CoqによるOpenFlowネットワークの形式化とFlowVisorの検証 [C3 (ポスター)]
逸見 港(1), 田辺 良則(2), 萩谷 昌己(1) ((1)東京大学 (2)国立情報学研究所)
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)
最大流を扱うプログラムに対する最悪テストケース生成 [C3 (ポスター)]
山口 洋 (東京大学)
決まった文法を持たないプログラミング言語の実現に向けて [C3 (ポスター)]
市川 和央, 千葉 滋 (東京工業大学 情報理工学研究科 数理・計算科学専攻)
アノテーションをもとにオブジェクトのデータレイアウトを自動的に変えるJavaコンパイラ [C3 (ポスター)]
汐田 徹也, 山口 洋, 千葉 滋 (東京大学情報理工学系研究科創造情報学専攻)
文脈移動法に基づく項書き換えシステムの自動変換 [C3 (ポスター・デモ)]
佐藤 洸一, 菊池 健太郎, 青戸 等人, 外山 芳人 (東北大学)
Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール [C3 (ポスター)]
宋 剛秀, 田村 直之, 番原 睦則 (神戸大学 情報基盤センター)
束縛変数を考慮した名目書き換えシステムの実現法 [C3 (ポスター・デモ)]
鈴木 貴樹, 菊池 健太郎, 青戸 等人, 外山 芳人 (東北大学)
依存型意味論による前提理論の形式化 [C3 (ポスター)]
石下 裕里, 戸次 大介 (お茶の水女子大学大学院 人間文化創成科学研究科 理学専攻 情報科学コース)
多段階計算の体系 $\lambda^\triangleright$ への持ち上げ操作の導入 [C3 (ポスター)]
花田 裕一朗, 五十嵐 淳 (京都大学工学部 京都大学大学院情報学研究科)
ドメイン特化言語処理系実装支援ライブラリのメタプログラミングによる実装 [C3 (ポスター・デモ)]
塩田 雅人, 岩崎 英哉 (電気通信大学大学院情報理工学研究科)
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 )
Neighborhood-sheafによる一階述語条件論理の意味論 [C3 (ポスター)]
山本 華子, 戸次 大介 (お茶の水女子大学大学院人間文化創成科学研究科)
Product lines implemented in feature-oriented programming are not sometimes object-oriented [C3 (ポスター)]
武山 文信 (東京工業大学 情報理工学研究科 数理・計算科学専攻)
ヘッダーファイルからSML#へのC関数の自動インポート [C3 (ポスター・デモ)]
相澤 遥也(1), 徳田 亮平(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学工学部 (2)東北大学電気通信研究所)
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)
Extending event-driven programming to support reactive programming by adding an inference mechanism [C3 (ポスター)]
莊 永裕 (東京大学 大学院 情報理工学系研究科 創造情報学専攻 千葉滋研究室)
CoqにおけるMonads with Predicate Liftingsの実装と考察 [C3 (ポスター)]
須田 啓司 (千葉大学大学院 理学研究科)
JavaCat: Realizing Context as Fluent [C3 (ポスター)]
紙名 哲生(1), 青谷 知幸(2), 増原 英彦(1) ((1)東京大学 (2)北陸先端科学技術大学院大学)
Rubyの操作的意味論の形式的定義に向けて [C3 (ポスター)]
深澤 優鷹(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院 情報科学研究科 (2)東北大学 電気通信研究所)
オブジェクト指向計算体系プロダクトラインの合併型による拡張 [C3 (ポスター)]
奥村 健太郎, 五十嵐 淳 (京都大学大学院 情報学研究科)
SML#のSQL統合へのgroup byの導入 [C3 (ポスター)]
斎藤 皓(1), 上野 雄大(2), 森畑 明昌(2), 大堀 淳(2) ((1)東北大学大学院 情報科学研究科 (2)東北大学 電気通信研究所)
不定元入り文字列を扱う言語XPCFの表現能力 [C3 (ポスター)]
寺山 慧, 立木 秀樹 (京都大学人間・環境学研究科)
正規言語の列挙: プログラミングへの応用 [C3 (ポスター・デモ)]
新屋 良磨 (東京工業大学大学院情報理工学研究科数理・計算科学科専攻佐々研究室)

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)
shift/reset 付きTDPEの抽出 [C1]
廣田 知子, 浅井 健一 (お茶の水女子大学)
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]
佐藤 悠史, 住井 英二郎 (東北大学大学院情報科学研究科)
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)
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.