jssst sig-ppl

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

発表時間:[C1] 25分、[C2] 20分、[C3] 2時間、[C4] 50分、[招待講演] 1時間 (いずれも質疑応答含む)

1日目午後の部 (3月8日 13:30-18:20)
13:30-13:35 オープニング
13:35-14:50 セッション1 継続 (座長:TBA)
Agdaによる依存型付きラムダ計算のCPS変換の実装 [C1]
叢 悠悠, 浅井 健一 (お茶の水女子大学)
shift/resetのselective CPS変換 [C1]
上原 千裕, 浅井 健一 (お茶の水女子大学)
A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations [C1]
Yusuke Miyazaki, Atsushi Igarashi (Graduate School of Informatics, Kyoto University)
14:50-15:05 休憩
15:05-16:05 セッション2 招待講演(1) (座長:TBA)
16:05-16:20 休憩
16:20-17:25 セッション3 論理、検証、高階文法 (座長:TBA)
コード生成に対するホーア論理の妥当性 [C1]
森口 草介 (関西学院大学)
A Debugger-Cooperative Higher-Order Contract System in Python [C2]
Ryoya Arai (1), Shigeyuki Sato (2), Hideya Iwasaki (1) ((1)University of Electro-Communications, (2)Kochi University of Technology)
出典: 14th Asian Symposium on Programming Languages and Systems (APLAS 2016)
On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic [C2]
Naoki Kobayashi (1), Etienne Lozes (2), Florian Bruse (3) ((1)University of Tokyo, (2)ENS Cachan, (3)University of Kassel)
出典: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
17:25-17:40 休憩
17:40-18:20 セッション4 検証、高階文法 (座長:TBA)
Stateful Manifest Contracts [C2]
Taro Sekiyama (1), Atsushi Igarashi (2) ((1)IBM Research-Tokyo, (2)Graduate School of Informatics, Kyoto University)
出典: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
On Word and Frontier Languages of Unsafe Higher-Order Grammars [C2]
Kazuyuki Asada, Naoki Kobayashi (University of Tokyo)
出典: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
1日目夜の部 (3月8日 20:00-22:00)
20:00-22:00 セッション5 ポスター・デモ(1) (座長:TBA)
逐次プログラムの停止性問題への帰着によるπ計算の停止性解析[C3(ポスター)]
石川 拓真(1), 塚田 武志(2), 小林 直樹(2) ((1)東京大学理学部情報科学科, (2)東京大学大学院情報理工学系研究科)
高階再帰スキームに対するStreettオートマトンモデル検査[C3(ポスター)]
鈴木 僚太(1), 塚田 武志(2), 小林 直樹(2) ((1)東京大学理学部情報科学科, (2)東京大学大学院情報理工学系研究科)
SMTソルバを用いた貪欲法・動的計画法の自動導出[C3(ポスター)]
奥山 裕也, 森畑 明昌 (東京大学)
Homotopies for Free![C3(ポスター)]
上村 太一 (京都大学)
Java用Fluent API生成システム "B2F" の設計と開発[C3(ポスター・デモ)]
中丸 智貴, 市川 和央, 山崎 徹郎, 千葉 滋 (東京大学 情報理工学系研究科 創造情報学専攻)
高階圧縮のための準線形空間アルゴリズム[C3(ポスター)]
Yuta Arichi, Takeshi Tsukada, Naoki Kobayashi (University of Tokyo)
拡張可能な作用とレコードのための統一的な骨組み[C3(ポスター・デモ)]
木下 郁章 (Tsuru Capital LLC)
C言語ヘッダからのATS言語関数シグニチャの自動生成と段階的な線形型の導入[C3(ポスター・デモ)]
岡部 究 (理化学研究所 計算科学研究機構)
グラフ書換え言語LMNtalの実行時処理系SLIMにおける制約付き部分グラフ探索の高速化[C3(ポスター)]
柳川 峻広, 上田 和紀 (Waseda University)
Balanced Double Queues for GC work stealing on Weak Memory Models[C3(ポスター)]
堀江 倫大, 堀井 洋, 小野寺 民也 (IBM Research - Tokyo)
深層学習によるプログラム生成の高速化[C3 (ポスター)]
今西 諒文(1), 関山 太朗(2), 村主 崇行(3), 末永 幸平(4) ((1)京都大学, (2)IBM Research - Tokyo, (3)理化学研究所, (4)京都大学 & JSTさきがけ)
Temporal Logics for Higher-Order Functional Programs based on Trace Semantics[C3(ポスター)]
Yuki Satake, Hiroshi Unno (University of Tsukuba)
漸進的型付き多相ラムダ計算[C3(ポスター)]
五十嵐 雄(1), 関山 太朗(2), 五十嵐 淳(1) ((1)京都大学,(2)IBM Research)
デバッグ能力強化によるプログラミング初学者向け学習法の設計[C3(ポスター)]
松上 寿支, 鍋島 英知 (山梨大学)
ベイジアン認知モデル設計のための 大脳皮質計算モデルの定式化の試み[C3(ポスター)]
尾崎 竜史, 一杉 裕志 (AIST)
SugarTracer: SAT型制約ソルバーSugarのトレースツール[C3(デモ)]
吉玉 元和(1), 寸田 智也(2), 南 雄之(2), 宋 剛秀(3), 番原 睦則(3), 田村 直之(3) ((1)神戸大学工学部情報知能工学科, (2)神戸大学大学院システム情報学研究科, (3)神戸大学情報基盤センター)
解集合プログラミングを用いた多層ナンバーリンクの解法[C3(ポスター・デモ)]
坡山 直樹(1), 川原 征大(2), 迫 龍哉(2), 宋 剛秀(3), 番原 睦則(3), 田村 直之(3) ((1)神戸大学工学部情報知能工学科, (2)神戸大学大学院システム情報学研究科, (3)神戸大学情報基盤センター)
マクロ森トランスデューサの実用的な型検査に向けて[C3(ポスター・デモ)]
阿部 和敬, 中野 圭介 (電気通信大学)
スタック領域のリンクリスト化によるメモリ効率の良い遅延スレッド生成に向けて[C3(ポスター)]
Yutaro Orikasa and Shigeru Chiba (The University of Tokyo)
汎言語健全構文マクロシステムの実装と課題[C3(ポスター・デモ)]
伊藤 玲於奈(1), 脇田 建(2) ((1)東京工業大学 理学部 情報科学科, (2)東京工業大学 情報理工学院)
統計的機械翻訳を利用したソースコードエディターに向けて[C3(ポスター)]
Yuki Kobayashi and Shigeru Chiba (University of Tokyo)
Bコンビネータの周期性について[C3(ポスター)]
池渕 未来(1), 中野 圭介(2) ((1)名古屋大学, (2)電気通信大学)
自己反映的な Garbage Collector の実現に向けた処理系の実装方式の提案[C3(ポスター)]
山崎 徹郎, 市川 和央, 千葉 滋 (The University of Tokyo)
意味的誤り検出ツールASTgrepのAST生成部の設計と実装[C3(ポスター)]
粕谷 彪人, 松田 直諒, 鵜川 始陽 (高知工科大学)
on-the-fly GCにおけるフェーズ変化時の書込みバリア切替え処理のモデル化[C3(ポスター)]
鵜川 始陽 (Kochi University of Technology)
超準関数型プログラミング言語NSF[C3(ポスター)]
中村 博文, 末永 幸平, 五十嵐 淳, 小島 健介 (京都大学情報学研究科)
検証済みコンパイラ CertSkel による GPGPU プログラム開発[C3(ポスター・デモ)]
朝倉 泉, 増原 英彦, 青谷 知幸 (東京工業大学)
Iterative Stencil Computations in Ruby on GPUs[C3(ポスター・デモ)]
Matthias Springer, Peter Wauligmann, Hidehiko Masuhara (Tokyo Institute of Technology)
メタラムダ計算を用いた限定継続への意味付け[C3(ポスター)]
戸澤 一成 (東京大学数理科学研究科)
2日目午前の部 (3月9日 9:00-12:10)
9:00-9:50 セッション6 SAT (座長:TBA)
SATソルバーの最新動向と利用技術 [C4]
宋 剛秀, 田村 直之 (神戸大学 情報基盤センター)

SAT ソルバーの求解性能が 2000 年以降飛躍的に向上している. さらに近年は単純に命題論理式の充足解を求めるだけでなく, 充足解が存在しない場合に,非充足となるような命題論理式の部分集合 (UNSAT コアと呼ばれる) を計算するなどの高度な機能も研究されている.
本サーベイ・チュートリアル発表では, SAT ソルバーに興味がある人, SATソルバーを使ってみたいと考えている人を対象に, SAT ソルバーの最新の動向および SAT 符号化,インクリメンタル SAT, Counterexample Guided Abstraction Refinement (CEGAR), UNSAT コアなど SAT ソルバーを利用するための技術を例を交えながら紹介する. 本発表を通じて SAT ソルバーを利用する面白さを共有できればと考えている.

9:50-10:00 休憩
10:00-10:40 セッション7 SAT、プログラム解析 (座長:TBA)
効率的なAllSATソルバーの実装と評価 [C2]
戸田 貴久 (電気通信大学) , 宋 剛秀 (神戸大学)
出典: ACM Journal of Experimental Algorithmics, Vol. 21
プログラム解析と統計手法の融合による定量的情報流解析 [C2]
Yusuke Kawamoto (1), Fabrizio Biondi (2), Axel Legay (2) ((1)AIST, Japan, (2)IRISA/INRIA Rennes)
出典: 21st International Conference on Formal Methods (FM 2016)
10:40-10:55 休憩
10:55-12:10 セッション8 グラフ処理 (座長:TBA)
Implementing distributed backpropagation algorithm using Apache Giraph [C1]
Amogh Rathore, Hideya Iwasaki (University of Electro-communications)
頂点部分集合変数を備えた大規模グラフ計算用領域特化言語 [C1]
定平 典久, 江本 健斗 (九州工業大学)
Push-Relabel アルゴリズムの頂点主体プログラミング [C1]
佐藤 重幸 (高知工科大学)
2日目午後の部 (3月9日 13:00-18:20)
13:00-14:00 セッション9 招待講演(2) (座長:TBA)
ビスケットのプログラミングテクニックと拡張案 [招待講演]
原田 康徳  (ビスケット開発者)
14:00-14:20 休憩
14:20-15:10 セッション10 マクロ、問い合わせ統合 (座長:TBA)
Foundational Theory of Self-Extendable Macros [C1]
Yuito Murase (University of Tokyo)
Sound and Efficient Full-featured Language-Integrated Query [C1]
勝島 達也, Oleg Kiselyov (Tohoku University)
15:10-15:25 休憩
15:25-16:30 セッション11 プログラム等価性、論理、検証 (座長:TBA)
木から文字列への決定性トップダウン変換の等価性判定の実装 [C1]
高橋 祐多 (電気通信大学 情報理工学部) , 中野 圭介 (電気通信大学 大学院 情報理工学研究科)
Approximate Relational Hoare Logic for Continuous Random Samplings [C2]
Tetsuya Sato (RIMS, Kyoto University)
出典: 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII)
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis [C2]
Kensuke Kojima (1), Minoru Kinoshita (2), Kohei Suenaga (1) ((1)Graduate School of Informatics, Kyoto University, (2)KLab Inc.)
出典: 23rd Static Analysis Symposium (SAS 2016)
16:30-16:45 休憩
16:45-17:25 セッション12 検証 (座長:TBA)
Verification of code generators via higher-order model checking [C2]
諏訪 敬之 (1), 塚田 武志 (1), 小林 直樹 (1), 五十嵐 淳 (2) ((1)東京大学大学院情報理工学系研究科, (2)京都大学大学院情報学研究科)
出典: 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2017)
Formalization of Karp-Miller Tree Construction on Petri Nets [C2]
山本 光晴 (1), 関根 祥吾 (2), 松本 早貴 (1) ((1)千葉大学, (2)株式会社アクロビジョン)
出典: 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)
17:25-17:40 休憩
17:40-18:20 セッション13 ラムダ計算、並行計算 (座長:TBA)
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence [C2]
Ryoma Sin'Ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada (University of Tokyo)
出典: 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)
A Truly Concurrent Game Model of the Asynchronous π-Calculus [C2]
Ken Sakayori, Takeshi Tsukada (University of Tokyo)
出典: 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)
2日目夜の部 (3月9日 20:00-22:00)
20:00-22:00 セッション14 ポスター・デモ(2) (座長:TBA)
Agdaによるダイクストラのアルゴリズムの証明[C3(ポスター)]
山田 麗, 浅井 健一 (お茶の水女子大学)
爆発則の再定式化および計算的構造[C3(ポスター)]
福田 陽介(1), 五十嵐 涼介(2) ((1)京都大学大学院情報学研究科, (2)京都大学大学院文学研究科)
協働ロボットCOROの開発における形式的仕様記述KMLの開発と適応[C3(ポスター)]
川口 順央, 忰山 豊 (ライフロボティクス株式会社)
マクロ展開過程を表示できるCプリプロセッサーの対話型評価環境の実装[C3(ポスター・デモ)]
今泉 良紀, 篠埜 功 (芝浦工業大学)
Introducing a Faster Inline-caching Mechanism for Method Seal[C3(ポスター)]
Wei Zhang (University of Tokyo)
多言語に対応した衛生的マクロ機構導入方式[C3(ポスター)]
高桑 健太郎, 渡部 卓雄 (東京工業大学)
Spark GraphXへのFregelコンパイラ[C3(ポスター)]
中島 拓, 江本 健斗 (九州工業大学)
型エラースライシングを利用した型エラーデバッガに関する実装と考察[C3(ポスター・デモ)]
脇川 奈穂(1), 対馬 かなえ(2), 浅井 健一 ((1)お茶の水女子大学,(2)国立情報学研究所)
グラフ照合のキャッシュ化による階層グラフ書換え言語LMNtalの高速化[C3(ポスター)]
Nozomi Matsuzawa, Kazunori Ueda (Waseda University)
無限状態システムのHFLモデル検査のための型に基づく手法[C3(ポスター)]
今井 雄毅(1), 小林 直樹(2), 佐藤 亮介(2), 末永 幸平(3), 塚田 武志(2) ((1)東京大学理学部情報科学科, (2)東京大学大学院情報理工学系研究科, (3)京都大学情報学研究科)
ジェネリックプログラミングを用いた証明木GUIライブラリの実装[C3(ポスター・デモ)]
松本 晴香, 浅井 健一 (お茶の水女子大学)
定理証明支援系CoqのプログラムからのSQLクエリの抽出[C3(ポスター・デモ)]
小澤 祐也, 中野 圭介 (電気通信大学)
Packrat Parsingを用いたRuby用パーサコンビネータライブラリWoodrat[C3(ポスター)]
佐藤 良祐, 池袋 教誉, 前田 敦司 (筑波大学)
イベントとシグナルを統合したJavaの軽量な拡張SignalJ[C3(ポスター)]
紙名 哲生(1), 青谷 知幸(2) ((1)立命館大学, (2)東京工業大学)
移動軌跡データ前処理の分散計算において要求される機能構造に関する一考察[C3(ポスター)]
横山 大作, 豊田 正史 (東京大学)
Coq上の証明項からの可読性の高い証明スクリプトの生成[C3(ポスター)]
山田 伊織, 中野 圭介 (電気通信大学)
メタインタプリタを用いた容易に拡張可能なモデル検査器の実装[C3(ポスター)]
恒川 雄太郎, 上田 和紀 (早稲田大学)
シンプルかつ明確な制約階層の再定式化に向けて[C3(ポスター)]
細部 博史 (法政大学)
C++プログラムにおける局所変数への参照の漏洩の検出[C3(ポスター・デモ)]
矢杉 和義, 五十嵐 淳 (京都大学大学院情報学研究科)
Kani-CUDAによるGPGPUプログラムの合成[C3(ポスター・デモ)]
蟹 暁, 朝倉 泉, 増原 英彦, 青谷 知幸 (東京工業大学)
Pregel+プログラムの性能解析[C3(ポスター)]
寺口 守, 佐藤 重幸, 松崎 公紀 (高知工科大学)
RTOSシステム状態の静的検証手法から見たATS言語とVeriFast検証器の比較[C3(ポスター・デモ)]
岡部 究 (理化学研究所 計算科学研究機構)
A Horn Constraint Solver based on Inductive Theorem Proving[C3(ポスター・デモ)]
Hiroki Sakamoto, Sho Torii, Shu Nakao, Hiroshi Unno (University of Tsukuba)
ライブプログラミング環境によるプログラマの行動と生産性への影響に関する実証研究[C3(ポスター)]
今井 朝貴, 増原 英彦, 青谷 知幸 (東京工業大学)
MetaOCamlによるGPGPUプログラミング[C3(ポスター)]
Oleg Kiselyov, 廣原 恵太 (Tohoku University)
Kanonライブプログラミング環境を用いたデータ構造のプログラミング[C3(ポスター・デモ)]
岡 明央, 増原 英彦, 今井 朝貴, 青谷 知幸 (東京工業大学)
Certified Mon{omorphiz|adific}ation of Gallina for Low-level Code Extraction[C3(ポスター・デモ)]
田中 哲(1), Reynald Affeldt(2), Jacques Garrigue (3) ((1)産業技術総合研究所, (2)AIST, (3)Nagoya University)
深さ優先探索と幅優先探索のBialgebraによる統一的記述[C3(ポスター)]
河田 透 (東京大学理学部情報科学科)
可逆計算のための高階プログラミング言語[C3(ポスター)]
西脇 友一 (東京大学情報理工学系研究科)
3日目午前の部 (3月10日 9:00-12:40)
9:00-9:50 セッション15 仮想マシン (座長:TBA)
ライブ仮想マシン移送の実現技術と最新動向について [C4]
山田 浩史 (東京農工大学)

本発表では,仮想マシン(VM)稼動させたまま別の物理マシンへと移動させるライブ VM 移送の実現技術とその最新動向について,およびライブ VM 移送技術とプログラミング言語分野との接点に迫ることで,新たな研究課題の発見を試みる.VM とは,VM モニタと呼ばれるソフトウェアによって提供される仮想的なハードウェアであり,これらを 1 台の物理マシンで複数作成することで複数の OS を同時に稼動できる.ライブ VM 移送は,VM を停止させることなく別のマシンへ移動できるため,VM の再配置による負荷分散や消費電力削減に効果的であることが知られている.技術的に興味深い部分が多く,著者を含め世界中の大学や企業において盛んに研究されている技術のひとつである.ライブ VM 移送の性能は VM の上で稼働しているプログラムの挙動に大きく依存しており,その挙動の把握や動作保証,最適化はライブ VM 移送の効率化および高機能化に大きく寄与するため,プログラミング言語分野で培われた手法はライブ VM 移送技術を発展させる可能性がある.

9:50-10:00 休憩
10:00-10:45 セッション16 プログラム変換 (座長:TBA)
属性文法合成による関数融合の実装 [C1]
中川 涼太, 中野 圭介 (電気通信大学 大学院 情報理工学研究科)
Stream Fusion, to Completeness [C2]
Oleg Kiselyov (1), Aggelos Biboudis (2), Nick Palladinos (3), Yannis Smaragdakis (2) ((1)Tohoku University, (2)University of Athens, (3)Nessos IT S.A. Athens)
出典: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
10:45-11:00 休憩
11:00-12:10 セッション17 論理、逆計算、組み込み言語 (座長:TBA)
Decision Procedure for Symbolic Heaps with Arrays [C1]
Daisuke Kimura (1), Makoto Tatsuta (2) ((1)Toho University, (2)National Institute of Informatics)
Clean Reversible Simulation of Ranking Binary Trees [C1]
大久保 雄飛, 横山 哲郎, 金山 知俊 (南山大学)
Eff Directly in OCaml [C2]
Oleg Kiselyov (1), Kc Sivaramakrishnan (2) ((1)Tohoku University, (2)University of Cambridge)
出典: ACM SIGPLAN Workshop on ML (ML 2016)
12:10-12:40 クロージング

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.