---------------------------------------------------------------------- 発表時間(含QA)：25分(C1,C2)，50分(C4) ---------------------------------------------------------------------- 3月7日(月) === オープニング 13:30〜13:35 === === セッション1 (並列計算) 13:35〜14:50 === 佐藤 重幸，田浦 健次朗 N体問題のためのデータ並列スケルトンの設計と実装 [C1] 朝倉 泉，増原 英彦，青谷 知幸 GPGPU向けデータ並列コードテンプレートの形式検証 [C1] Kazuaki Ishizaki, Akihiro Hayashi, Gita Koblents and Vivek Sarkar Compiling and Optimizing Java 8 Programs for GPU Execution [C2] 出典：The 24th International Conference on Parallel Architectures and Compilation Techniques (PACT 2015) === セッション2 (招待講演1) 15:10〜16:10 === 奥田 遼介 ディープラーニングフレームワークとChainerの実装 === セッション3 (プロセス計算，並行計算) 16:30〜17:45 === 服部 浩二，櫻川 貴司 セッション間の干渉のある型付きプロセス計算とその応用 [C1] Yuya Uezato and Yasuhiko Minamide Synchronized Recursive Timed Automata [C2] 出典：The 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-20) Ugo Dal Lago, Claudia Faggian, Benoît Valiron and Akira Yoshimizu Parallelism and Synchronization in an Infinitary Context [C2] 出典：Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015) === ポスター・デモセッション 19:45〜22:00 === 3月8日(火) === セッション5 (項書換え系，関数型プログラミング言語) 9:00〜10:40 === 浜名 誠 プログラミング言語研究のための(高階)項書換え系入門 [C4] Oleg Kiselyov and Hiromi Ishii Freer Monads, More Extensible Effects [C2] 出典：Haskell Symposium 2015 (Haskell'15) オレッグ・キセリョーヴ 埋込み確率プログラミング言語とその漸進評価 [C1] === セッション6 (型理論，形式言語，分離論理) 10:55〜12:10 === Takeshi Tsukada and Koji Nakazawa Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild [C1] 新屋 良磨 言語の測度に基づく非正規性の証明技法 [C1] Makoto Tatsuta and Daisuke Kimura Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic [C1] === セッション7 (DSL，言語処理) 13:00〜14:15 === Hiroshi Yamaguchi and Shigeru Chiba Inverse Macro in Scala [C2] 出典：14th International Conference on Generative Programming: Concepts & Experience (GPCE’15) 那須 孝志，滝本 宗宏 依存関係に基づく分岐融合 [C1] 江本 健斗，松崎 公紀，胡 振江，森畑 明昌，岩崎 英哉 大規模グラフ並列処理のための関数型領域特化言語 [C1] === セッション8 (招待講演) 14:30〜15:30 === Julia Lawall Finding the right level of abstraction: Program analysis and the Linux kernel === セッション9 (形式化，対話的定理証明器) 15:45〜17:00 === 奥村 健太郎，小島 健介，五十嵐 淳 SIMT のための Hoare 論理の Coq を用いた形式化と並列 prefix-sum アルゴリズムの検証 [C1] Akira Tanaka, Reynald Affeldt and Jacques Garrigue Formal Verification of the rank Function for Succinct Data Structures [C1] 門脇 香子，浅井 健一 Agda による定式化された型推論器の拡張と改良 [C1] === セッション10 (メタプログラミング) 17:10〜18:00 === オレッグ・キセリョーヴ MetaOCamlにおける最適コード生成 [C4] === ポスター・デモセッション 19:45〜22:00 === 3月9日(水) === セッション12 (構文解析，関数型プログラムの解析と評価) 9:00〜10:40 === 市川 和央 ビジュアル構文解析 [C4] 松下 翼，篠埜 功 関数適用によるギャップを考慮したコードクローンの検出および除去に関する研究 [C1] 森畑 明昌 代数的性質に基づくラムダ式の並列評価 [C1] === セッション13 (テスト，検証，仕様と実装) 11:00〜12:15 === 兼行 大将，番原 睦則，宋 剛秀，田村 直之，井上 克巳，沖本 天太 解集合プログラミングを用いた制約組合せテストケース生成 [C1] 青木 利晃，千葉 勇輝，松原 正裕，成沢 文雄 ISO26262のための安全要求記述言語と追跡可能性検証手法の提案 [C1] 山本 和彦 HTTP/2の実装手法とヘッダ圧縮の簡潔化 [C1] === クロージング 12:15〜12:45 === ---------------------------------------------------------------------- カテゴリ3（ポスター・デモ発表） 採択リスト（順不同) 宮原 一喜，橋本 健二，関 浩之 非決定性木変換器における問合せ保存 迫 龍哉, 川原 征大，Takehide Soh, Mutsunori Banbara, Naoyuki Tamura and Hidetomo Nabeshima インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー Yang Bai and Isao Sasano LR構文解析のエラー回復機能を用いたキーワード補完機能の系統的導出 坂口 和彦，亀山 幸義 Coq/SSReflect の extraction の改善 Yuichi Nishiwaki 高級フィールド計算: 自己安定化するフィールド計算のための万能プログラミング言語 Matthias Springer and Hidehiko Masuhara Ikra: Leveraging Object-oriented Abstractions in a Ruby-to-CUDA JIT Translator 神野 祐磨，菊池 健太郎，青戸 等人，外山 芳人 項書き換えシステムの基底合流性の自動検証 小野沢 倖太，菊池 健太郎，青戸 等人，外山 芳人 高階書き換えシステムの合流性自動検証ツール 西村 進 組合せトポロジーによる分散並列プロトコル発見アルゴリズム Yuji Yoneda and Yoshiaki Takata プログラムの構造を短く指定することによるコード補完手法の提案 阿部 晃典，住井 英二郎 機械学習による関数型ブーリアンプログラムの型推論 Frédéric Bour and Jacques Garrigue Implementing Modular Implicits for OCaml 宮﨑 勇輔，関山 太朗，五十嵐 淳 限定継続演算子 shift/reset のための漸進的型付け Yuito Murase 衛生的マクロにおけるリテラル識別子に関する要件 Jun Yoneyama Java PathFinderによるMQTTクライアントライブラリの検証 Satoshi Ogasawara Alloyによる論理データモデルの運用 石崎 一明，Jan Wróblewski，小原 盛幹 GPUを用いたApache Sparkプログラムの高速化 渡部 恭久，亀山 幸義 1MLのサブセット言語に対する型システムの構築 Yuta Iwama, Kazuhiro Ichikawa and Shigeru Chiba 動的型付き言語上での構文拡張により発生する曖昧性の回避について 恒川 雄太郎，上田 和紀 グラフ書き換え言語LMNtalにおける第一級書き換え規則の設計と実装 松澤 望，上田 和紀 グラフ書換え言語 LMNtal のビジュアルプログラミング環境の開発 叢 悠悠，浅井 健一 動的束縛を用いた stepper の実装 Tomoharu Ugawa and Hideya Iwasaki Androidにおける部分コンパクションの実装 叢 悠悠 高校生向け OCaml プログラミング体験授業の設計 Yuki Ishii and Kenichi Asai 強い型付けを利用したプログラミング初学者のための開発環境 重本 孝太，八杉 昌宏，平石 拓，馬谷 誠二 HOPEコンパイラの実装に向けて Kodai Hashimoto, Sho Torii and Hiroshi Unno Automating Total Correctness Verification of Higher-Order Functional Programs with Algebraic Data Types 良本 海, 八杉 昌宏，平石 拓，馬谷 誠二 仮想環境を考慮した要求駆動型負荷分散の検討 Ryo Okugawa, Hidehiko Masuhara and Tomoyuki Aotani Featherweight JavaのMeta-Theory a la Carteを利用した拡張可能な形式化フレームワーク Kiyoshi Ogawa 母語方式による言語教育の成果と課題 渡邉 慶一, 佐藤 亮介，塚田 武志，小林 直樹 高階関数型プログラムの公平停止性の自動反証手法 Ruochen Huang, Hidehiko Masuhara and Tomoyuki Aotani RPythonを用いたErlang仮想機械PyrlangにおけるJITコンパイル方針の改良 酒寄 健，塚田 武志 非同期π計算の真に並行なゲーム意味論 Keita Watanabe, Hidehiko Masuhara and Tomoyuki Aotani 多次元的文脈指向言語Korzのメソッドディスパッチの改善 安武 祥平，渡部 卓雄 Actario: 定理証明支援系Coqによるアクターシステムの検証 木下 大輔，中野 圭介 OCamlの関数からCoqの帰納的述語への変換に向けて 丹治 将貴, 中野 圭介，岩崎 英哉 Rubyに対するGradual typingの導入に向けて Joseph Caldwell Examining ABI-Induced Overhead in ARM Microcontrollers Hiroki Sakamoto and Hiroshi Unno Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types 本多 健太郎 抽象解釈と量子スタビライザー形式による量子プログラムのもつれ解析 Kanae Tsushima 型エラープログラムの自動分析・修正の提案 倉光 君郎 新しい教育用プログラミング言語の設計を考える 畑中 涼，松崎 公紀 プログラム高速化の効果の検証 －超解像処理を題材として－ Tomohisa Osada and Shigeru Chiba 密な演算子呼び出しで実現した内部DSLの別途処理記述による実行速度改善の試み Nariyoshi Chida and Kimio Kuramitsu 先読み付き正規表現の決定性有限オートマトンによるマッチングの実装 Xu Li Why Does Calculation Coverage Testing Require Huge Memory? Tetsuro Yamazaki, Yoshiki Sato and Shigeru Chiba 包含文字列の内部char配列を共有化する拡張文字列を部分的に利用した時の性能を調べる実験 Masanori Sato, Shun Honda and Kimio Kuramitsu 双方向変換による逆構文解析器の自動生成 Oleg Kiselyov 拡張された拡張可能作用 Oleg Kiselyov MetaOCamlデモ Shin Saito, Takaaki Tateishi, Futoshi Iwama, Hiroki Yanagisawa, Yoichi Hatsutori and Toshinari Itoko 証明の抽象化と機械学習による自動定理証明に基づくプログラム生成 井上 健太 3人の賢者の問題とその推論の妥当性のCoqにおける証明 ---------------------------------------------------------------------- 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.