jssst sig-ppl

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

[1日目午後の部 | 1日目夜の部 | 2日目午前の部 | 2日目午後の部 | 2日目夜の部 | 3日目午前の部]

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

1日目午後の部 (3月5日 13:30-18:30)
13:30-13:40 オープニング
13:40-14:50 セッション1 API，並列計算 (座長：増原 英彦（東京工業大学）)
Silverchain: A Fluent API Generator [C2]
Tomoki Nakamaru, Kazuhiro Ichikawa, Tetsuro Yamazaki , Shigeru Chiba (The University of Tokyo)
出典  16th International Conference on Generative Programming: Concepts and Experience (GPCE 2017)
Fregelコンパイラにおける不要な値送受信の削減 [C1]
加藤 直斗, 岩崎 英哉 (電気通信大学)
木上の非構造的再帰関数の融合－高速N体問題解法の場合－ [C1]
佐藤 重幸 (高知工科大学)
14:50-15:05 休憩
15:05-16:05 セッション2 招待講演(1) (座長：松崎 公紀（高知工科大学）)
演繹から帰納へ~新しいシステム開発パラダイム ［講演資料］
丸山　宏 (株式会社Preferred Networks 最高戦略責任者)
概要を表示
概要  深層機械学習はそのパラメタの多さの故に、任意の多次元非線形関数を近似することができ、その意味で擬似的にチューリング完全な計算モデルと見なすことができる。その結果、問題をモデル化しそれをアルゴリズムとして実装する、という今までの演繹的な手法ではなく、問題の入出力を与えて実装をほぼ自動的に生成するという、帰納的な方法が、実用的なシステム開発手法として視野に入ってきた。近い将来、ITシステムの大半が帰納的に開発されることになるかもしれない。この講演では、プログラミングパラダイムとしての深層機械学習の可能性と本質的な限界、実用化に向けての課題について議論する。 概要を隠す
16:05-16:25 休憩
16:25-17:30 セッション3 高階言語，コード生成 (座長：南出 靖彦（東京工業大学）)
Pumping Lemma for Higher-order Languages [C2]
Kazuyuki Asada(1), Naoki Kobayashi(2) ((1)The University of Tokyo (2)The University of Tokyo)
出典 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Refined Environment Classifiers: Type- and Scope-Safe Code Generation with Mutable Cells [C2]
Oleg Kiselyov(1), Yukiyoshi Kameyama (2), Yuto Sudo(3) ((1)Tohoku University (2)University of Tsukuba (3)University of Tsukuba)
出典 14th Asian Symposium on Programming Languages and Systems (APLAS 2016)
コード生成計算とハイブリッド論理 [C1]
山崎駿介, オレッグ・キセリョーヴ (東北大学)
17:30-17:45 休憩
17:45-18:30 セッション4 言語設計 (座長：勝股 審也（国立情報学研究所）)
A Nonstandard Functional Programming Language [C2]
Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi (Kyoto University)
出典 15th Asian Symposium on Programming Languages and Systems (APLAS 2017)
限定継続命令をもつ依存型付き言語の設計 [C1]
叢 悠悠, 浅井 健一 (お茶の水女子大学)
1日目夜の部 (3月5日 20:00-22:00)
20:00-22:00 セッション5 ポスター・デモ(1) (座長：平石 拓（京都大学）)
高次特異値分解（HOSVD）のnモード行列展開を応用した立体パズルの求解 [C3 (ポスター)]
山本 直樹, 石田 明男, 大石 信弘, 村上 純 (熊本高等専門学校)
π計算の変種の圏論的モデル [C3 (ポスター)]
酒寄 健, 塚田 武志 (東京大学)
ContextWorkflow: 中断と償いのためのDSL [C3 (ポスター・デモ)]
井上 裕昭(1), 青谷 知幸(2), 五十嵐 淳(1) ((1)京都大学 (2)東京工業大学)
Dependent Temporal Effects and Fixpoint Logic for Verification [C3 (ポスター)]
Yoji Nanjo(1), Hiroshi Unno(1), Eric Koskinen(2), Tachio Terauchi(3) ((1)University of Tsukuba (2)Stevens Institute of Technology (3)Waseda University)
メタ混合JITコンパイラの提案 [C3 (ポスター)]
伊澤 侑祐, 増原 英彦, 青谷 知幸 (東京工業大学)
多者間通信プロトコルに対するタイムアウトの導入 [C3 (ポスター)]
松原 信忠, 結縁 祥治 (名古屋大学)
SPIN用メモリモデルライブラリmmlibを使った並行コピーGCのモデル検査 [C3 (ポスター・デモ)]
飯干 寛幸, 松元 稿如, 鵜川 始陽 (高知工科大学)
Monadic Reflectionの判断的再構成 [C3 (ポスター)]
河田 透 (東京大学)
文脈様相に基づく可逆プログラミング言語 [C3 (ポスター)]
西脇 友一, 田辺 弘太郎 (東京大学)
継続渡しスタイルの関数型プログラミング言語における並行処理の設計と実装 [C3 (ポスター)]
小島 渚, 島 和之 (広島市立大学)
階層型行列の区分け決定処理のCilk Plusによる並列化 [C3 (ポスター)]
白 正陽(1), 平石 拓(2), 伊田 明弘(3), 中島 浩(2) ((1)京都大学情報学研究科 (2)京都大学学術情報メディアセンター (3)東京大学情報情報基盤センター)
分散システムを対象としたモデルベーステストにおけるテストオラクルの高速化 [C3 (ポスター)]
坂西 一暁(1), Cyrille Artho(2), 田辺 良則(3), 萩谷 昌己(1), 北村 崇師(4) ((1)東京大学 (2)KTH Royal Institute of Technology (3)鶴見大学文学部ドキュメンテーション学科 (4)産業技術総合研究所)
JavaのStream APIによるストリーム操作の停止性を検査する型システム [C3 (ポスター)]
長谷川 健太(1), 吉田 真也(1), 桑原 寛明(2), 上原 哲太郎(1), 國枝 義敏(1) ((1)立命館大学 (2)南山大学)
帰納的述語を含む分離論理によるプログラム検証のためのループ不変式の導出 [C3 (ポスター)]
仲田 壮佑(1), 中澤 巧爾(2) ((1)名古屋大学大学院 情報科学研究科 (2)名古屋大学大学院 情報学研究科)
定理証明支援系Coqにおける証明木を操作可能なインタフェースの設計および実装 [C3 (ポスター・デモ)]
早川 恵太, 中野 圭介 (電気通信大学)
X10: Performance and Productivity at Scale [C3 (ポスター)]
竹内 幹雄, 水田 秀行 (日本アイ・ビー・エム（株）東京基礎研究所)
組合せ最適化問題を記述するための関係代数の集合上への拡張 [C3 (ポスター)]
坂梨 元軌, 酒井 正彦, 西田 直樹, 橋本 健二 (名古屋大学情報学研究科)
確率的高階不動点論理 [C3 (ポスター)]
三谷 庸, 小林 直樹, 塚田 武志 (東京大学)
OCaml ステッパの拡張 [C3 (ポスター・デモ)]
古川 つきの, 浅井 健一 (お茶の水女子大学)
Packrat parsingを用いたRuby用パーサコンビネータライブラリWoodratのデバッグ拡張 [C3 (ポスター)]
坂上 知紀, 池袋 教誉, 前田 敦司 (筑波大学)
Traf: Coqでの対話的証明と連動した証明木描画ツール [C3 (ポスター・デモ)]
木村 麻衣(1), 田中 雄太(2), 川端 英之(1), 弘中 哲夫(1) ((1)広島市立大学 (2)関電システムソリューションズ)
C言語用packrat parser構築ライブラリCPEGを用いたRuby字句解析器の実装 [C3 (ポスター)]
杉本 優太, 前田 敦司 (筑波大学　システム情報工学研究科)
生放送ストリーム中継システムのCoqによる形式化と検証 [C3 (ポスター・デモ)]
安武 祥平, 今井 宜洋 (DWANGO Co., Ltd.)
ホスト言語をJavaとするDSLを用いたエミュレータの自動生成 [C3 (ポスター・デモ)]
奧田 勝己(1), 千葉 滋(2) ((1)三菱電機（株）先端技術総合研究所/東京大学情報理工学系研究科 (2)東京大学情報理工学系研究科)
気楽なアプリケーション開発を可能にするSearch-Select-Superpose Loopの反復支援ツール [C3 (ポスター・デモ)]
西本 匡志, 西山 佳志, 川端 英之, 弘中 哲夫 (広島市立大学)
小規模組込みシステム向けFRP言語のアクターモデルにもとづく実行系 [C3 (ポスター)]
渡部 卓雄 (東京工業大学)
木構造を辿る高階プログラムの最適化に向けて [C3 (ポスター)]
阿部 和敬, 中野 圭介 (電気通信大学 大学院情報理工学専攻)
Streaming String Transducerの合成の形式的証明 [C3 (ポスター)]
赤間 仁志, 南出 靖彦 (東京工業大学 情報理工学院)
アクターシステムを対象としたリバースデバッギングフレームワークActoverseへのAOPの導入 [C3 (ポスター)]
柴内 一宏, 渡部 卓雄 (東京工業大学)
並列分散フレームワークの耐障害性評価のための通信障害模擬機能 [C3 (ポスター)]
西牟禮 亮(1), 八杉 昌宏(2), 平石 拓(3), 馬谷 誠二(4) ((1)九州工業大学情報工学部知能情報工学科 (2)九州工業大学大学院情報工学研究院 (3)京都大学学術情報メディアセンター (4)京都大学大学院情報学研究科)
2日目午前の部 (3月6日 9:00-12:35)
9:00-9:50 セッション6 チュートリアル (1) (座長：西崎 真也（東京工業大学）)
二種類の高階モデル検査とプログラム検証の関係について [C4] ［講演資料］
Naoki Kobayashi (The University of Tokyo)
概要を表示
概要  有限状態モデル検査は，システム検証手法としてハードウェアやソフトウェアの検証に応用されてきた．近年，HORSモデル検査，HFLモデル検査という2種類の異なる高階拡張が提案されている．前者は，高階再帰スキーム（HORS）と呼ばれる高階文法によって生成される無限木が与えられる性質を満たすか否かを判定する問題であり，後者は，有限状態遷移システムが高階様相不動点論理（HFL）の論理式によって表現される性質を満たすか否かを判定する問題である．本チュートリアルでは，これら二つの高階モデル検査の概念を解説した後，両者に密接な対応関係が存在すること，および高階関数型プログラムの検証問題がこれらの問題に自然に帰着できることを示す． 概要を隠す
9:50-10:05 休憩
10:05-11:10 セッション7 プログラム検証・証明 (1) (座長：対馬 かなえ（国立情報学研究所）)
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs [C2]
Hiroshi Unno(1), Yuki Satake(2), Tachio Terauchi(3) ((1)University of Tsukuba (2)University of Tsukuba (3)Waseda University)
出典 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018)
Streett Automata Model Checking of Higher-Order Recursion Schemes [C2]
Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada (The University of Tokyo)
出典 Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Coqにおける手続き的証明から宣言的証明への変換 [C1]
山田 伊織, 中野 圭介 (電気通信大学)
11:10-11:25 休憩
11:25-12:35 セッション8 プログラム検証・証明 (2) (座長：田辺 良則（鶴見大学）)
A Guess-and-Assume Approach to Loop Fusion for Program Verification [C2]
Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi (Kyoto University)
出典 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018)
条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明 [C1]
栗田 泰智, 青戸 等人 (新潟大学)
AgdaによるPHOASを用いたCPS変換の正当性の証明 [C1]
石尾 千晶, 山田 麗, 浅井 健一 (お茶の水女子大学)
2日目午後の部 (3月6日 13:45-18:40)
13:45-14:45 セッション9 招待講演(2) (座長：西崎 真也（東京工業大学）)
情報教育とプログラミング教育: 私達は当事者である(べき)かも?［講演資料］
久野 靖 (電気通信大学)
概要を表示
概要  私達コンピュータサイエンスの専門家にとって、情報教育、プログラミング教育はかなり縁遠いものかも知れません。それは例えば、扱っていることがらのレベルがかなり違うので、初心者のことまで考えていられない、ということかも知れません。しかし私達のこの分野は、後継者が少なければ衰退してしまうでしょうし、それは困ります。そうならないためには「教育」が大切になります。本講演は、皆様があまり聞く機会がないであろう「教育」について、講演者がこれまで関わってきた事柄を中心に紹介させていただき、議論のきっかけとなることを企図しています。 概要を隠す
14:45-15:05 休憩
15:05-15:55 セッション10 プログラム理解 (座長：江本 健斗（九州工業大学）)
関数型言語の初学者のためのHaskellのビジュアルプログラミング環境 [C1]
近松 万由子, 岩崎 英哉, 中野 圭介 (電気通信大学)
複数の型エラースライスによるill-typedプログラムの分析 [C1]
対馬 かなえ(1), 佐藤 重幸(2) ((1)国立情報学研究所 (2)高知工科大学)
15:55-16:10 休憩
16:10-17:20 セッション11 言語処理系 (座長：鵜川 始陽（高知工科大学）)
拡張SC言語で記述したSchemeインタプリタによる計算状態操作機構の評価 [C1]
八杉 昌宏(1), 池内 嶺知(2), 平石 拓(3), 小宮 常康(4), 重本 孝太(5) ((1)九州工業大学大学院情報工学研究院 (2)九州工業大学情報工学部知能情報工学科（現在，株式会社ユードム） (3)京都大学学術情報メディアセンター (4)電気通信大学大学院情報理工学研究科 (5)九州工業大学大学院情報工学府)
実用的な型エラースライサーの提案と評価 [C1]
脇川 奈穂(1), 対馬 かなえ(2) ((1)お茶の水女子大学 (2)国立情報学研究所)
Buffered Garbage Collection for Self-Reflective Customization [C2]
Tetsuro Yamazaki, Shigeru Chiba (The University of Tokyo)
出典 33rd ACM/SIGAPP Symposium On Applied Computing (SAC 2018)
17:20-17:35 休憩
17:35-18:40 セッション12 プログラミング言語機能 (座長：前田 敦司（筑波大学）)
Session-ocaml: a Session-based Library with Polarities and Lenses [C2]
Keigo Imai(1), Nobuko Yoshida(2), Shoji Yuen(3) ((1)Gifu University (2)Imperial College London (3)Nagoya University)
出典  19th International Conference on Coordination Models and Languages (COORDINATION 2017)
スタック構造の累積引数を持つ関数を融合するための木変換器合成 [C1]
西山 舜, 中野 圭介 (電気通信大学)
Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation [C2]
江木 聡志 (楽天技術研究所)
出典  The Scheme and Functional Programming Workshop 2017
2日目夜の部 (3月6日 20:00-22:00)
20:00-22:00 セッション13 ポスター・デモ(2) (座長：平石 拓（京都大学）)
属性付き記号的木変換器の合成 [C3 (ポスター)]
中川 涼太, 中野 圭介 (電気通信大学大学院情報理工学研究科)
情報教育の参照基準 [C3 (ポスター)]
久野 靖 (電気通信大学)
階層グラフ書換え言語LMNtalのパターンマッチにおける否定と全称量化の実現 [C3 (ポスター)]
齋藤 諒人, 上田 和紀 (早稲田大学)
IoTソフトウェアのための不安定なネットワークとデバイスをシミュレートするモデルベーステスト [C3 (ポスター)]
米山 惇(1), Cyrille Artho(2), 萩谷 昌己(1), 田辺 良則(3) ((1)東京大学 (2)KTH Royal Institute of Technology (3)鶴見大学)
スカラー仮引数・テンソル仮引数による微分幾何の記法のプログラミングへの導入 [C3 (ポスター・デモ)]
江木 聡志 (楽天技術研究所)
先読み・後読みをもつ正規表現の有限状態オートマトンへの変換 [C3 (ポスター)]
藤浪 大弥 (日本大学文理学部ドイツ文学科)
グラフ書換え系から共有メモリ並列プログラムを生成する手法の検討 [C3 (ポスター)]
冨岡 太一, 上田 和紀 (早稲田大学)
補助関数付きの関数型プログラムの自動合成 [C3 (ポスター)]
江口 慎悟, 小林 直樹, 塚田 武志 (東京大学)
競技プログラミングのデータを用いたクローン検出 [C3 (ポスター)]
Daniel Perez Hernandez, 千葉 滋 (東京大学)
言語仮想機械におけるカスタマイズ可能なごみ集めモジュールの実装 [C3 (ポスター)]
赤澤 亮弥(1), 鵜川 始陽(2), 岩﨑 英哉(1) ((1)電気通信大学 (2)高知工科大学)
非決定的顕在的契約計算 [C3 (ポスター)]
西田 雄気, 五十嵐 淳 (京都大学)
Ruby言語へのGradual Typingの実装 [C3 (ポスター・デモ)]
宮澤 修, 中野 圭介 (電気通信大学)
既存のソースコード群を利用したコーディングスタイルの推定 [C3 (ポスター)]
松永 智將, 千葉 滋 (東京大学)
人間的動作を活かしたライブコーディングのためのソフトウェアシステム [C3 (ポスター)]
佐藤 輝年, 千葉 滋 (東京大学)
言語の包含判定に基づくサニタイズ文脈の自動決定 [C3 (ポスター)]
高橋 和也(1), 南出 靖彦(2) ((1)東京工業大学 理学部 情報科学科 (2)東京工業大学 情報理工学院)
安全な多チャネル通信とリソース管理のための型システム [C3 (ポスター)]
服部 浩二, 櫻川 貴司 (京都大学大学院 人間・環境学研究科)
手続き型動的型付け言語に対するリージョン推論の導入 [C3 (ポスター)]
齋地 崇大, 前田 敦司 (筑波大学)
配列を含むC言語サブセットから難解言語Malbolgeへのコンパイラ [C3 (ポスター・デモ)]
岩金 カナン(1), 坂梨 元軌(2), 酒井 正彦(2), 西田 直樹(2), 橋本 健二(2) ((1)名古屋大学工学部 (2)名古屋大学情報学研究科)
解集合プログラミングによるクラウド利用者の都合を考慮したメンテナンススケジューリング [C3 (ポスター・デモ)]
奥野 伸吾, 飯倉 二美, 渡辺 幸洋 (富士通研究所)
置換の自動証明タクティク [C3 (ポスター・デモ)]
坂口 和彦 (筑波大学)
構文解析器の動的拡張による衛生的マクロ機構の実現 [C3 (ポスター)]
高桑 健太郎, 渡部 卓雄 (東京工業大学)
グラフ上の生成検査集約プログラミングの実現に向けて [C3 (ポスター)]
中島 拓, 江本 健斗 (九州工業大学)
Coqにおける可読性の高い形式的証明に向けて [C3 (ポスター)]
村田 康佑, 江本 健斗 (九州工業大学)
Java ソースコードを読みやすくする合字の利用法 [C3 (ポスター・デモ)]
中丸 智貴, 千葉 滋 (東京大学)
証明支援器Coqを使ったプログラミング言語の操作的意味論に基づく型安全性の拡張可能な形式化の研究 [C3 (ポスター)]
奥河 諒, 青谷 知幸, 増原 英彦 (東京工業大学)
Coqによる簡潔データ構造のライブラリに向けての今後の課題 [C3 (ポスター)]
田中 哲(1), Reynald Affeldt(1), Jacques Garrigue(2) ((1)産業技術総合研究所 (2)名古屋大学)
tagless-final・extensible-effectsから機械自然言語理解まで [C3 (ポスター・デモ)]
Oleg Kiselyov (Tohoku University)
型プロバイダを用いた解析木に対する型タグの静的な送出法 [C3 (ポスター)]
髙林 佳稀, 山口 大輔, 倉光 君郎 (横浜国立大学)
解析表現文法の一般化に関する研究 [C3 (ポスター)]
多田 拓, 山口 大輔, 倉光 君郎 (横浜国立大学)
プログラミング言語へのバージョンの導入の研究 [C3 (ポスター)]
田辺 裕大(1), 青谷 知幸(2), 増原 英彦(2) ((1)東京工業大学理学部情報科学科 (2)東京工業大学情報理工学院)
3日目午前の部 (3月7日 9:00-12:45)
9:00-9:50 セッション14 チュートリアル (2) (座長：松崎 公紀（高知工科大学）)
チュートリアル：ブロックチェーンの計算モデル [C4] ［講演資料］
齋藤 新, 吉濱 佐知子 (日本アイ･ビー･エム株式会社東京基礎研究所)
概要を表示
概要  ブロックチェーン (分散台帳技術)については仮想通貨やビジネスアプリケーションの実装インフラとして，また法的な取り扱いについて議論されることが多い．しかし，様々なブロックチェーンの実装が出現するなか，それらが持つ分散システムとしての安全性などについての詳細な議論はなおざりにされがちである．実際，2016年にはシステムとプログラムのバグをついた約65億円の内部通貨流出事件が発生している．厳密な議論のためには，その計算モデルを正しく捉えることが非常に重要であり，我々プログラミング理論の専門家の得意とするところである．本チュートリアルでは主要なブロックチェーンの実装を取り上げ，それらの計算モデルについて概説する．また、それらが満たすべき様々な性質についても説明する． 概要を隠す
9:50-10:05 休憩
10:05-10:50 セッション15 プログラム解析，高速化 (座長：倉光 君郎（横浜国立大学）)
ブロックチェーンにおけるチェーンコードの決定性の解析 [C1]
岩間 太, 立石 孝彰, 齋藤 新, 天野 俊一, 吉濱 佐知子 (日本IBM)
Accelerating Spark Datasets by Inlining Deserialization [C2]
Jan Wróblewski(1), Kazuaki Ishizaki(2), Hiroshi Inoue(3), Moriyoshi Ohara(4) ((1)University of Warsaw (2)IBM Research - Tokyo (3)IBM Research - Tokyo (4)IBM Research - Tokyo)
出典 31st IEEE International Parallel & Distributed Processing Symposium (IPDPS 2017)
10:50-11:05 休憩
11:05-12:15 セッション16 プログラミング言語理論 (座長：新屋 良磨（秋田大学）)
Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic [C2]
Stefano Berardi(1), Makoto Tatsuta(2) ((1)University of Torino (2)National Institute of Informatics)
出典 32nd Annual IEEE Symposium on Logic in Computer Science (LICS2017)
Decidability of Entailments in Separation Logic with Arrays and Lists [C1]
Daisuke Kimura(1), Makoto Tatsuta(2) ((1)Toho University (2)National Institute of Informatics)
高階契約に対するトレース意味論の完全抽象性 [C1]
井上 鉄也,  中澤 巧爾 (名古屋大学大学院情報学研究科)
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.