jssst sig-ppl

第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
プログラム

[1日目午後の部 | 1日目夜の部 | 2日目午前の部 | 2日目午後の部 | 2日目夜の部 | 3日目午前の部]
1日目午後の部 (3月7日 13:30-17:45)
13:30-13:35 オープニング
13:35-14:50 セッション1 並列計算 (座長：八杉 昌宏(九州工業大学))
N体問題のためのデータ並列スケルトンの設計と実装 [C1]
佐藤 重幸，田浦 健次朗  (東京大学大学院情報理工学系研究科電子情報学専攻)
GPGPU向けデータ並列コードテンプレートの形式検証 [C1]
朝倉 泉，増原 英彦，青谷 知幸  (東京工業大学)
Compiling and Optimizing Java 8 Programs for GPU Execution [C2]
Kazuaki Ishizaki(1), Akihiro Hayashi(2), Gita Koblents(3) and Vivek Sarkar(2)  ((1)IBM Research - Tokyo (2)Rice University (3)IBM Canada)
出典： The 24th International Conference on Parallel Architectures and Compilation Techniques (PACT 2015)
14:50-15:10 休憩
15:10-16:10 セッション2 招待講演(1) (座長：鵜川 始陽(高知工科大学))
ディープラーニングフレームワークとChainerの実装 [招待講演]
奥田 遼介 (Preferred Networks)
16:10-16:30 休憩
16:30-17:45 セッション3 プロセス計算，並行計算 (座長：角谷 良彦(東京大学))
セッション間の干渉のある型付きプロセス計算とその応用 [C1]
服部 浩二，櫻川 貴司  (京都大学大学院 人間・環境学研究科)
Synchronized Recursive Timed Automata [C2]
Yuya Uezato(1) and Yasuhiko Minamide(2)  ((1)University of Tsukuba (2)Tokyo Institute of Technology)
出典： The 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-20)
Parallelism and Synchronization in an Infinitary Context [C2]
Ugo Dal Lago(1), Claudia Faggian(2), Benoît Valiron(3) and Akira Yoshimizu(4)  ((1)Univ. di Bologna & INRIA (2)CNRS & Univ. Paris Diderot (3)CentraleSupélec & LRI, Univ. Paris Sud (4)Univ. of Tokyo)
出典： Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015)
1日目夜の部 (3月7日 19:45-22:00)
19:45-22:00 セッション4 ポスター・デモ(1) (座長：海野 広志(筑波大学))
非決定性木変換器における問合せ保存 [C3 (ポスター)]
宮原 一喜(1)，橋本 健二(2)，関 浩之(2)  ((1)奈良先端科学技術大学院大学 (2)名古屋大学)
インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー [C3 (ポスター・デモ)]
迫 龍哉(1)，川原 征大(1)，宋 剛秀(2), 番原 睦則(2), 田村 直之(2)，鍋島 英知(3)  ((1)神戸大学 (2)神戸大学 情報基盤センター (3)山梨大学)
LR構文解析のエラー回復機能を用いたキーワード補完機能の系統的導出 [C3 (ポスター・デモ)]
白 楊，篠埜 功  (芝浦工業大学)
Coq/SSReflect の extraction の改善 [C3 (デモ)]
坂口 和彦，亀山 幸義  (筑波大学)
高級フィールド計算: 自己安定化するフィールド計算のための万能プログラミング言語 [C3 (ポスター)]
西脇 友一  (東京大学)
Ikra: Leveraging Object-oriented Abstractions in a Ruby-to-CUDA JIT Translator [C3 (ポスター)]
Matthias Springer and Hidehiko Masuhara  (Tokyo Institute of Technology)
組合せトポロジーによる分散並列プロトコル発見アルゴリズム [C3 (ポスター)]
西村 進  (京都大学)
機械学習による関数型ブーリアンプログラムの型推論 [C3 (ポスター・デモ)]
阿部 晃典，住井 英二郎  (東北大学)
Implementing Modular Implicits for OCaml [C3 (デモ)]
Frédéric Bour(1) and Jacques Garrigue(2)  ((1)Sponsored by Jane Street Group LLC (2)Nagoya University)
Java PathFinderによるMQTTクライアントライブラリの検証 [C3 (ポスター)]
米山 惇  (東京大学)
グラフ書き換え言語LMNtalにおける第一級書き換え規則の設計と実装 [C3 (ポスター)]
恒川 雄太郎，上田 和紀  (早稲田大学)
グラフ書換え言語 LMNtal のビジュアルプログラミング環境の開発 [C3 (ポスター・デモ)]
松澤 望，上田 和紀  (早稲田大学)
動的束縛を用いた stepper の実装 [C3 (ポスター・デモ)]
叢 悠悠，浅井 健一  (お茶の水女子大学)
Androidにおける部分コンパクションの実装 [C3 (ポスター)]
鵜川 始陽(1)，岩崎 英哉(2)  ((1)高知工科大学 (2)電気通信大学)
強い型付けを利用したプログラミング初学者のための開発環境 [C3 (ポスター・デモ)]
石井 柚季，浅井 健一  (お茶の水女子大学)
HOPEコンパイラの実装に向けて [C3 (ポスター)]
重本 孝太(1)，八杉 昌宏(2)，平石 拓(3)，馬谷 誠二(4)  ((1)九州工業大学 情報工学部 (2)九州工業大学 大学院情報工学研究院 (3)京都大学 学術情報メディアセンター (4)京都大学 大学院情報学研究科)
仮想環境を考慮した要求駆動型負荷分散の検討 [C3 (ポスター)]
良本 海(1)，八杉 昌宏(2)，平石 拓(3)，馬谷 誠二(4)  ((1)九州工業大学　情報工学部 (2)九州工業大学 大学院情報工学研究院 (3)京都大学 学術情報メディアセンター (4)京都大学 大学院情報学研究科)
Featherweight JavaのMeta-Theory a la Carteを利用した拡張可能な形式化フレームワーク [C3 (ポスター)]
奥河 諒，増原 英彦，青谷 知幸  (東京工業大学)
母語方式による言語教育の成果と課題 [C3 (ポスター)]
小川 清  (名古屋市工業研究所)
高階関数型プログラムの公平停止性の自動反証手法 [C3 (ポスター)]
渡邉 慶一(1)，佐藤 亮介(2)，塚田 武志(2)，小林 直樹(2)  ((1)東京大学理学部情報科学科 (2)東京大学大学院情報理工学系研究科)
RPythonを用いたErlang仮想機械PyrlangにおけるJITコンパイル方針の改良 [C3 (ポスター)]
黄 若塵，増原 英彦，青谷 知幸  (東京工業大学)
多次元的文脈指向言語Korzのメソッドディスパッチの改善 [C3 (ポスター)]
渡邉 恵大，増原 英彦，青谷 知幸  (東京工業大学)
Rubyに対するGradual typingの導入に向けて [C3 (ポスター)]
丹治 将貴，中野 圭介，岩崎 英哉  (電気通信大学)
プログラム高速化の効果の検証 －超解像処理を題材として－ [C3 (ポスター)]
畑中 涼，松崎 公紀  (高知工科大学)
Why Does Calculation Coverage Testing Require Huge Memory? [C3 (ポスター)]
Xu Li  (Graduate School of Information Science and Technology, The University of Tokyo)
拡張された拡張可能作用 [C3 (ポスター)]
オレッグ・キセリョーヴ  (東北大学)
2日目午前の部 (3月8日 9:00-12:10)
9:00-10:40 セッション5 項書換え系，関数型プログラミング言語 (座長：佐藤 亮介(東京大学))
プログラミング言語研究のための(高階)項書換え系入門[C4] スライド
浜名 誠  (群馬大学 理工学府)
Freer Monads, More Extensible Effects [C2]
Oleg Kiselyov(1) and Hiromi Ishii(2)  ((1)Tohoku University (2)University of Tsukuba)
出典： Haskell Symposium 2015 (Haskell'15)
埋込み確率プログラミング言語とその漸進評価 [C1]
オレッグ・キセリョーヴ  (東北大学大学院情報科学研究科)
10:40-10:55 休憩
10:55-12:10 セッション6 型理論，形式言語，分離論理 (座長：安部 達也(千葉工業大学))
Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild [C1]
Takeshi Tsukada(1) and Koji Nakazawa(2)  ((1)The University of Tokyo (2)Nagoya University)
言語の測度に基づく非正規性の証明技法 [C1]
新屋 良磨  (東京工業大学 数理・計算科学専攻)
Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic [C1]
Makoto Tatsuta(1) and Daisuke Kimura(2)  ((1)National Institute of Informatics (2)Toho University)
2日目午後の部 (3月8日 13:00-18:00)
13:00-14:15 セッション7 DSL，言語処理 (座長：平石 拓(京都大学))
Inverse Macro in Scala [C2]
Hiroshi Yamaguchi and Shigeru Chiba  (The University of Tokyo)
出典： 14th International Conference on Generative Programming: Concepts & Experience (GPCE’15)
依存関係に基づく分岐融合 [C1]
那須 孝志(1)，滝本 宗宏(2)  ((1)東京理科大学理工学研究科情報科学専攻 (2)東京理科大学)
大規模グラフ並列処理のための関数型領域特化言語 [C1]
江本 健斗(1)，松崎 公紀(2)，胡 振江(3)，森畑 明昌(4)，岩崎 英哉(5)  ((1)九州工業大学 (2)高知工科大学 (3)国立情報学研究所 (4)東京大学 (5)電気通信大学)
14:15-14:30 休憩
14:30-15:30 セッション8 招待講演(2) (座長：青戸 等人(新潟大学))
Finding the right level of abstraction: Program analysis and the Linux kernel [招待講演]
Julia Lawall (Inria)
15:30-15:45 休憩
15:45-17:00 セッション9 形式化，対話的定理証明器 (座長：森口 草介(関西学院大学))
SIMT のための Hoare 論理の Coq を用いた形式化と並列 prefix-sum アルゴリズムの検証 [C1]
奥村 健太郎(1)，小島 健介(1,2)，五十嵐 淳(1,2)  ((1)京都大学大学院情報学研究科 (2)JST CREST)
Formal Verification of the rank Function for Succinct Data Structures [C1]
Akira Tanaka(1), Reynald Affeldt(1) and Jacques Garrigue(2)  ((1)National Institute of Advanced Industrial Science and Technology (2)Nagoya University)
Agda による定式化された型推論器の拡張と改良 [C1]
門脇 香子，浅井 健一  (お茶の水女子大学大学院 人間文化創成科学研究科)
17:00-17:10 休憩
17:10-18:00 セッション10 メタプログラミング (座長：中野 圭介(電気通信大学))
MetaOCamlにおける最適コード生成 [C4] ウェブページとソースコードpower.ml, filter.ml
オレッグ・キセリョーヴ  (東北大学大学院情報科学研究科)
2日目夜の部 (3月8日 19:45-22:00)
19:45-22:00 セッション11 ポスター・デモ(2) (座長：海野 広志(筑波大学))
項書き換えシステムの基底合流性の自動検証 [C3 (ポスター)]
神野 祐磨(1)，菊池 健太郎(1)，青戸 等人(2)，外山 芳人(1)  ((1)東北大学 電気通信研究所 (2)新潟大学)
高階書き換えシステムの合流性自動検証ツール [C3 (ポスター)]
小野沢 倖太(1)，菊池 健太郎(1)，青戸 等人(2)，外山 芳人(1)  ((1)東北大学 電気通信研究所 (2)新潟大学)
プログラムの構造を短く指定することによるコード補完手法の提案 [C3 (ポスター・デモ)]
米田 裕司，高田 喜朗  (高知工科大学)
限定継続演算子 shift/reset のための漸進的型付け [C3 (ポスター)]
宮﨑 勇輔(1)，関山 太朗(2)，五十嵐 淳(2)  ((1)京都大学工学部情報学科 (2)京都大学大学院情報学研究科)
衛生的マクロにおけるリテラル識別子に関する要件 [C3 (ポスター)]
村瀬 唯斗  (東京大学)
Alloyによる論理データモデルの運用 [C3 (ポスター)]
小笠原 啓  (ITプランニング)
GPUを用いたApache Sparkプログラムの高速化 [C3 (ポスター・デモ)]
石崎 一明(1)，Jan Wróblewski(2)，小原 盛幹(1)  ((1)IBM Research - Tokyo (2)University of Warsaw)
1MLのサブセット言語に対する型システムの構築 [C3 (ポスター)]
渡部 恭久，亀山 幸義  (筑波大学)
動的型付き言語上での構文拡張により発生する曖昧性の回避について [C3 (ポスター)]
岩間 雄太，市川 和央，千葉 滋  (東京大学)
高校生向け OCaml プログラミング体験授業の設計 [C3 (ポスター)]
叢 悠悠  (お茶の水女子大学)
Automating Total Correctness Verification of Higher-Order Functional Programs with Algebraic Data Types [C3 (ポスター・デモ)]
Kodai Hashimoto, Sho Torii and Hiroshi Unno  (University of Tsukuba)
非同期π計算の真に並行なゲーム意味論 [C3 (ポスター)]
酒寄 健(1)，塚田 武志(2)  ((1)東京大学理学部情報科学科 (2)東京大学大学院情報理工学系研究科)
Actario: 定理証明支援系Coqによるアクターシステムの検証 [C3 (ポスター)]
安武 祥平，渡部 卓雄  (東京工業大学)
OCamlの関数からCoqの帰納的述語への変換に向けて [C3 (ポスター)]
木下 大輔，中野 圭介  (電気通信大学)
Examining ABI-Induced Overhead in ARM Microcontrollers [C3 (ポスター)]
Joseph Caldwell  (University of Tokyo)
Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types [C3 (ポスター・デモ)]
Hiroki Sakamoto and Hiroshi Unno  (University of Tsukuba)
抽象解釈と量子スタビライザー形式による量子プログラムのもつれ解析 [C3 (ポスター)]
本多 健太郎  (東京大学)
型エラープログラムの自動分析・修正の提案 [C3 (ポスター)]
対馬 かなえ  (国立情報学研究所)
新しい教育用プログラミング言語の設計を考える [C3 (ポスター・デモ)]
倉光 君郎  (横浜国立大学)
密な演算子呼び出しで実現した内部DSLの別途処理記述による実行速度改善の試み [C3 (ポスター)]
長田 朋久，千葉 滋  (東京大学)
先読み付き正規表現の決定性有限オートマトンによるマッチングの実装 [C3 (ポスター・デモ)]
千田 忠賢，倉光 君郎  (横浜国立大学)
包含文字列の内部char配列を共有化する拡張文字列を部分的に利用した時の性能を調べる実験 [C3 (ポスター)]
山崎 徹郎，佐藤 芳樹，千葉 滋  (東京大学)
双方向変換による逆構文解析器の自動生成 [C3 (ポスター・デモ)]
佐藤 正典，本多 峻，倉光 君郎  (横浜国立大学)
MetaOCamlデモ [C3 (デモ)]
オレッグ・キセリョーヴ  (東北大学)
証明の抽象化と機械学習による自動定理証明に基づくプログラム生成 [C3 (ポスター)]
齋藤 新, 立石 孝彰，岩間 太，柳澤 弘揮，初鳥 陽一，井床 利生  (日本IBM 東京基礎研究所)
3人の賢者の問題とその推論の妥当性のCoqにおける証明 [C3 (ポスター)]
井上 健太  (千葉大学大学院)
3日目午前の部 (3月9日 9:00-12:45)
9:00-10:40 セッション12 構文解析，関数型プログラムの解析と評価 (座長：滝本 宗宏(東京理科大学))
ビジュアル構文解析 [C4] スライド
市川 和央  (東京大学情報理工学研究科)
関数適用によるギャップを考慮したコードクローンの検出および除去に関する研究 [C1]
松下 翼，篠埜 功  (芝浦工業大学大学院 理工学研究科 電気電子情報工学専攻)
代数的性質に基づくラムダ式の並列評価 [C1]
森畑 明昌  (東京大学大学院総合文化研究科)
10:40-11:00 休憩
11:00-12:15 セッション13 テスト，検証，仕様と実装 (座長：田辺 良則(鶴見大学))
解集合プログラミングを用いた制約組合せテストケース生成 [C1]
兼行 大将(1)，番原 睦則(2)，宋 剛秀(2)，田村 直之(2)，井上 克巳(3)，沖本 天太(4)  ((1)神戸大学大学院システム情報学研究科 (2)神戸大学 情報基盤センター (3)国立情報学研究所 情報学プリンシプル研究系 (4)神戸大学 海事科学部)
ISO26262のための安全要求記述言語と追跡可能性検証手法の提案 [C1]
青木 利晃(1)，千葉 勇輝(1)，松原 正裕(2)，成沢 文雄(2)  ((1)北陸先端科学技術大学院大学 情報科学研究科 (2)(株) 日立製作所 研究開発グループ 制御イノベーションセンタ)
HTTP/2の実装手法とヘッダ圧縮の簡潔化 [C1]
山本 和彦  (IIJ イノベーションインスティテュート)
12:15-12:45 クロージング

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.