jssst sig-ppl

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

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

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

1日目午後の部 (3月6日 13:30-17:30)
13:30-13:40 オープニング
13:40-14:20 セッション1 仮想マシン実装 (座長：前田 敦司（筑波大学）)
アプリケーションに特化したJavaScript仮想機械開発のためのユニットテストを用いたプロファイリング [C1]
片岡 崇史(1), 鵜川 始陽(1), 岩崎 英哉(2) ((1)高知工科大学 (2)The University of Electro-Communications)
JavaScript 仮想機械記述のためのドメイン特化言語 [C1]
高野 保真(1), 鵜川 始陽(2), 岩崎 英哉(3) ((1)青山学院大学 (2)高知工科大学 (3)The University of Electro-Communications)
14:20-14:40 休憩
14:40-15:50 セッション2 招待講演 (1) (座長：末永 幸平（京都大学）)
プログラミング教育の現在と未来---特にプログラミング分野専門家への期待
萩谷 昌己 (東京大学)
概要  小学校や中学校のプログラミング教育についても触れながら、高等学校の情報科の新しい学習指導要領、高等学校の情報教育の現状と課題について述べるとともに、高等学校と接続する大学共通教育としての情報教育の現状とそのあるべき姿について論じる。 小学校から大学、特に情報の非専門家のための基礎教育に至る一環した情報教育の可能性についても触れる。 特にその中でプログラミング教育の重要性について述べ、プログラミング分野専門家が求められていること、さらに、プログラミング教育におけるプログラミング研究の可能性について論じる。
15:50-16:10 休憩
16:10-17:30 セッション3 型 (座長：Jacques Garrigue（名古屋大学）)
Dynamic type inference for gradual Hindley?Milner typing [C2]
Yusuke Miyazaki(1), Taro Sekiyama(2), Atsushi Igarashi(1) ((1)Kyoto University (2)National Institute of Informatics)
空間効率の良いコアーション計算のためのコアーション渡し形式 [C1]
津田 優也(1), 五十嵐 淳 (1) ((1)Kyoto University)
動的変数をもつ依存型付きラムダ計算 [C1]
叢 悠悠(1), 浅井 健一(2) ((1)お茶の水女子大学 (2)Ochanomizu University)
Progress report: Ruby 3における静的型解析の実現に向けて [C1]
遠藤 侑介(1), 松本 宗太郎(2), 上野 雄大(3), 住井 英二郎(4), 松本 行弘(5) ((1)Cookpad Inc. (2)Sider株式会社 (3)東北大学電気通信研究所 (4)東北大学大学院情報科学研究科 (5)(一財)Rubyアソシエーション)
1日目夜の部 (3月6日 19:00-22:00)
19:00-22:00 セッション4 ポスター・デモ (1) (座長：浅田 和之（東北大学）)
Introduction of Ruby 3 Challenges [C3]
笹田 耕一(1), 遠藤 侑介(1) ((1)クックパッド株式会社)
スタック領域における時間的メモリ安全性を保証するための静的解析手法の開発と実装（ポスター・デモ） [C3]
矢杉 和義(1), 五十嵐 淳(1) ((1)Kyoto University)
LALR 文法検査を備えた fluent API ライブラリを Scala で実装する (ポスター) [C3]
Tetsuro Yamazaki(1), Tomoki Nakamaru(1), Shigeru Chiba(1) ((1)The University of Tokyo)
カバレッジ誘導機構をもつ深層学習型文法ベースファジング(ポスター) [C3]
實成 優馬(1), 荒堀 喜貴(1), 権藤 克彦(1) ((1)Tokyo Institute of Technology)
深層学習型文法ベースファジングの比較実験(ポスター) [C3]
實成 優馬(1), 荒堀 喜貴(1), 権藤 克彦(1) ((1)Tokyo Institute of Technology)
双文脈判断に基づくプログラミング言語と次数付き代数的効果（ポスター） [C3]
西脇 友一(1), 内藏 理史(1) ((1)The University of Tokyo)
シャロー項書換えシステムに対するUN性の効率的な決定手続き (ポスター・デモ) [C3]
山口 真央生(1), 青戸 等人(1) ((1)新潟大学)
バックトラックによる正規表現マッチングの計算量判定の実装（ポスター） [C3]
高橋 和也(1), 南出 靖彦(1) ((1)Tokyo Institute of Technology)
先読み付き正規表現と解析表現の微分 [C3]
Takayuki Miyazaki(1), Yasuhiko Minamide(1) ((1)Tokyo Institute of Technology)
セキュリティ特性を表現するためのトレース等価と認識論理(ポスター) [C3]
南 規楽(1) ((1)Kyoto University)
グループ化機能を持つ統合言語クエリに対する正規化 [C3]
大倉 瑠維(1), 亀山 幸義(1) ((1)University of Tsukuba)
モジュールのコード生成におけるコード爆発問題の解決（ポスター） [C3]
佐藤 佑飛(1), 亀山 幸義(1) ((1)University of Tsukuba)
Coqを用いた高度なプログラム運算定理の検証に向けて（ポスター） [C3]
村田 康佑(1), 江本 健斗(1) ((1)九州工業大学)
FregelからGraphXへのコンパイルにおけるSMTソルバを用いた不要な通信の削減（ポスター） [C3]
小西 篤志(1), 江本 健斗(1) ((1)九州工業大学)
述語抽象化と反例駆動抽象化改良による自動νHFL(Z)モデル検査（ポスター） [C3]
鈴木 僚太(1), 小林 直樹(1), 塚田 武志(1) ((1)The University of Tokyo)
頂点主体並列分散処理のメッセージ送信遅延による通信数削減 (ポスター) [C3]
加藤 直斗(1), 岩崎 英哉(1) ((1)The University of Electro-Communications)
プッシュダウン付き木変換器の逆像型検査（ポスター） [C3]
西山 舜(1), 中野 圭介(2) ((1)The University of Electro-Communications (2)東北大学)
シーケンス変換を用いた命題論理の自動証明 [C3]
Masanori Kanahara(1), Ryosuke Sato(1), Naoyasu Ubayashi(1), Yasutaka Kamei(1) ((1)Kyushu University)
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4 [C3]
Yosuke Fukuda(1), Akira Yoshimizu(2) ((1)Kyoto University (2)INRIA)
NetKAT with Cryptography [C3]
菅原 慎之介(1), 住井 英二郎(1) ((1)東北大学大学院情報科学研究科)
関数型プログラムの反例を用いた条件式の自動修正（ポスター） [C3]
松井 健(1), 佐藤 亮介(2), 鵜林 尚靖(2), 亀井 靖高(2) ((1)九州大学工学部電気情報工学科 (2)九州大学大学院システム情報科学研究院)
ブロックチェーン合意形成プロトコルのCoqによる証明からのコード抽出 [C3]
木村 朝輝(1), 住井 英二郎(2) ((1)東北大学 工学部 電気情報物理工学科 住井・松田研究室 (2)東北大学 大学院 情報科学研究科)
余帰納的証明におけるガード条件の漸進的検査および自動化支援(ポスター・デモ) [C3]
小澤 祐也(1), 中野 圭介(2) ((1)電気通信大学 大学院情報理工学研究科 情報・ネットワーク工学専攻 (2)東北大学 電気通信研究所)
所有権型を利用した CHC ベースのプログラム検証 [C3]
松下 祐介(1), 小林 直樹(1), 塚田 武志(1) ((1)The University of Tokyo)
高階関数型プログラムのための時相論理 (ポスター) [C3]
奥山 裕也(1), 塚田 武志(1), 小林 直樹(1) ((1)The University of Tokyo)
循環証明体系における準カット除去可能性について(ポスター) [C3]
早乙女 献自(1), 中澤 巧爾(1) ((1)Nagoya University)
Python プロジェクトで使用されるライブラリ数の調査（ポスター） [C3]
Chao-Ling Chang(1), 上田 裕己(1), 石尾 隆(1), 松本 健一(1) ((1)奈良先端科学技術大学院大学)
線形時相論理による計算効果の発生の型レベル表現（ポスター） [C3]
Yuta Sato(1) ((1)神戸大学)
ワンショットの代数的効果から非対称コルーチンへの変換 (ポスター･デモ) [C3]
河原 悟(1), 亀山 幸義(2) ((1)筑波大学 プログラム論理研究室 (2)University of Tsukuba)
Progress report: Ruby 3における静的型解析の実現に向けて [C3]
遠藤 侑介(1), 松本 宗太郎(2), 上野 雄大(3), 住井 英二郎(4), 松本 行弘(5) ((1)Cookpad Inc. (2)Sider株式会社 (3)東北大学電気通信研究所 (4)東北大学大学院情報科学研究科 (5)(一財)Rubyアソシエーション)
コード移動に基づく分岐発散低減(ポスター) [C3]
福原 淳司(1), 滝本 宗宏(1) ((1)東京理科大学)
2日目午前の部 (3月7日 9:00-12:00)
9:00-10:20 セッション5 論理とプログラム検証 (座長：関山 太朗（国立情報学研究所）)
Propositional Dynamic Logic for Higher-Order Functional Programs [C2]
Yuki Satake(1), Hiroshi Unno(1) ((1)University of Tsukuba)
A Fixpoint Logic and Dependent Effects for Temporal Property Verification [C2]
Yoji Nanjo(1), Hiroshi Unno(1), Eric Koskinen(2), Tachio Terauchi(3) ((1)University of Tsukuba (2)Stevens Institute of Technology, United States (3)Waseda University)
Failure of Cut-Elimination in Cyclic Proofs of Separation Logic [C1]
Daisuke Kimura(1), Koji Nakazawa(2), Tachio Terauchi(3), Hiroshi Unno(4) ((1)Toho University (2)Nagoya University (3)Waseda University (4)University of Tsukuba)
Spatial Factorization in Cyclic-Proof System for Separation Logic [C1]
Koji Nakazawa(1), Makoto Tatsuta(2), Daisuke Kimura(3), Mitsuru Yamamura(1) ((1)Nagoya University (2)National Institute of Informatics (3)Toho University)
10:20-10:40 休憩
10:40-12:00 セッション6 プログラム合成 (座長：森畑 明昌（東京大学）)
数値や文字列に対するガードを含む累積引数付き再帰関数の融合 [C1]
棚橋 健人(1), 中野 圭介(2) ((1)The University of Electro-Communications (2)東北大学, 電気通信研究所)
Automated Synthesis of Functional Programs with Auxiliary Functions [C2]
Shingo Eguchi(1), Naoki Kobayashi(1), Takeshi Tsukada(1) ((1)The University of Tokyo)
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks [C2]
Taro Sekiyama(1), Kohei Suenaga(2) ((1)National Institute of Informatics (2)Kyoto University)
プロファイル型プログラム合成によるGPGPUプログラムの半自動最適化 [C1]
蟹 暁(1), 増原 英彦(1), 青谷 知幸(1) ((1)Tokyo Institute of Technology)
2日目午後の部 (3月7日 13:00-17:00)
13:00-14:00 セッション7 招待講演 (2) (座長：笹田 耕一（クックパッド）)
lldリンカ：次世代の標準開発環境を目指したソフトウェアの開発
植山 類 (Google)
概要  LLVMプロジェクトは、LLVMコンパイラ・バックエンドだけではなく、C/C++フロントエンドのClangやLLDBデバッガなど、コンパイラ・ツールチェイン全体を提供することを目標の一つとしています。 その中でプロダクション品質のリンカが存在していないことは長らくプロジェクトの課題になっていましたが、講演者はメイン開発者としてlldリンカの開発を行うことでその課題を解決しました。 lldは既存のGNUリンカと互換性がありつつも数倍高速であり、FreeBSDやOpenBSDなどの標準リンカとして採用されているほか、主要なコンソールゲーム機や、大規模ウェブサイトの内部など、様々な場所で広く使われています。 この講演では、人気のあるオープンソースソフトウェアを作るために講演者が考えていたことや、ハイパフォーマンスかつシンプルなデザインのプログラムを書くための考え方などについて話をします。
14:00-14:20 休憩
14:20-15:20 セッション8 プログラミング環境 (座長：遠藤 侑介（クックパッド）)
BlocklyをベースにしたOCamlビジュアルプログラミングエディタ [C1]
松本 晴香(1), Kenichi Asai(2) ((1)お茶の水女子大学 (2)Ochanomizu University)
Mining Source Code Improvement Patterns from Similar Code Review Works [C2]
Yuki Ueda(1), Takashi Ishio(1), Akinori Ihara(2), Kenichi Matsumoto(1) ((1)Nara Institute of Science and Technology (2)Wakayama University)
On Defining Recursive Functions in Live Data Structure Programming [C1]
Akio Oka(1), Hidehiko Masuhara(1), Tomoyuki Aotani(1) ((1)Tokyo Institute of Technology)
15:20-15:40 休憩
15:40-17:00 セッション9 プログラミング言語 (座長：Oleg Kiselyov（東北大学）)
Linear Quipper: 埋め込み線形型付き量子プログラミング言語 [C1]
菅野 翔太(1), 松田 一孝(1), Oleg Kiselyov(1) ((1)東北大学大学院情報科学研究科)
Non-linear Pattern Matching with Backtracking for Non-free Data Types [C2]
Satoshi Egi(1), Yuichi Nishiwaki(2) ((1)Rakuten Institute of Technology (2)The University of Tokyo)
HOBiT: Programming Lenses Without Using Lens Combinators [C2]
Kazutaka Matsuda(1), Meng Wang(2) ((1)Tohoku University (2)University of Bristol, UK)
Harmonizing Signals and Events with a Lightweight Extension to Java [C2]
Tetsuo Kamina(1), Tomoyuki Aotani(2) ((1)Oita University (2)Tokyo Institute of Technology)
2日目夜の部 (3月7日 19:00-22:00)
19:00-22:00 セッション10 ポスター・デモ (2) (座長：浅田 和之（東北大学）)
GUIベースのパーサジェネレータの検討 [C3]
奥田 勝己(1), 千葉 滋(2) ((1)東京大学 情報理工学系研究科/三菱電機 先端技術総合研究所 (2)東京大学情報理工学系研究科)
バージョン付きモジュールシステムの提案 [C3]
Yudai Tanabe(1), Tomoyuki Aotani(1), Hidehiko Masuhara(1) ((1)Tokyo Institute of Technology)
OCaml Blocklyデモ（ポスター・デモ） [C3]
松本 晴香(1), Kenichi Asai(2) ((1)お茶の水女子大学 (2)Ochanomizu University)
ニューラルネットワークにおける表現可能なデータ数のSSReflectによる形式化 [C3]
井上 健太(1), 山本 光晴(2) ((1)千葉大学大学院　理学研究科 (2)千葉大学大学院理学研究院)
DSLのための型システム指定言語「METACO」 [C3]
Haochen Xie(1) ((1)Nagoya University)
グラフの内包記法の実現に向けたLMNtalにおけるメッシュ構造の定義検討(ポスター) [C3]
田村 滉明(1), 上田 和紀(1), 冨岡 太一(1) ((1)Waseda University)
ペトリネットにおける有界性に関する性質のCoq/SSReflectによる形式化 [C3]
稲垣 衛(1), 山本 光晴(2) ((1)千葉大学大学院融合理工学府 (2)千葉大学大学院理学研究院)
組込みシステム向けFRP言語における動的動作のための抽象化（ポスター） [C3]
松村 有倫(1), 渡部 卓雄(1) ((1)Tokyo Institute of Technology)
プログラミング言語の非終端記号の獲得に向けたSkip-Gramモデルの利用 [C3]
Tomomasa Matsunaga(1), Shigeru Chiba(1) ((1)The University of Tokyo)
分散並行バグ動的検出の大規模性能シミュレータ [C3]
片平 遥香(1), 荒堀 喜貴(1) ((1)Tokyo Institute of Technology)
型に基づく実用的な HFL モデル検査アルゴリズム [C3]
細井 洋吉(1), 小林 直樹(1), 塚田 武志(1) ((1)The University of Tokyo)
ハイブリッド制約処理系HyLaGIへの共通部分式除去を用いた式の簡約の導入 [C3]
山田 悠之介(1), 上田 和紀(1) ((1)Waseda University)
アプリケーションに特化したJavaScript仮想機械開発のためのユニットテストを用いたプロファイリング [C3]
片岡 崇史(1), 鵜川 始陽(1), 岩崎 英哉(2) ((1)高知工科大学 (2)The University of Electro-Communications)
等価性検査のための入力×イベント空間の探査経験則の学習 [C3]
冨永 江奈(1), 荒堀 喜貴(1), 権藤 克彦(1) ((1)Tokyo Institute of Technology)
実用的な型エラースライサーの評価およびデータ活用に向けた取り組み（ポスター・デモ） [C3]
Naho Wakikawa(1), Kenichi Asai(1), Kanae Tsushima(2) ((1)Ochanomizu University (2)NII)
TypeScriptライブラリに対するSemantic Versioningにおける互換性の定式化及びそれに基づくバージョン決定アルゴリズム [C3]
藤浪 大弥(1), 笠井 信宏(2) ((1)日本大学文理学部ドイツ文学科 (2)芝浦工業大学工学部情報工学科)
Z定理を用いたラムダ・ミュー計算の合流性証明（ポスター） [C3]
本多 雄樹(1), 中澤 巧爾(1), 藤田 憲悦(2) ((1)Nagoya University (2)群馬大学)
セッション型、簡潔に (ポスター・デモ) [C3]
オレッグ キセリョーヴ(1), 今井 敬吾(2) ((1)Tohoku University (2)岐阜大学)
ハイブリッド制約処理系HyLaGIにおける分枝限定法を用いた離散変化時刻導出手法 [C3]
佐藤 柾史(1), 上田 和紀(1) ((1)Waseda University)
スマートコントラクト のためのEffectively Callback-Free性の型に基づく静的検証 [C3]
Hiromasa Saito(1), Atsushi Igarashi(1), Kohei Suenaga(1), Yuki Nishida(1) ((1)Kyoto University)
依存型プログラムの型付AST [C3]
田中 哲(1) ((1)National Institute of Advanced Industrial Science and Technology (AIST))
Incremental な OCaml ステッパの開発 [C3]
古川 つきの(1), 浅井 健一(1) ((1)お茶の水女子大学)
組込みシステム向けFRP言語に対する第一級関数の導入（ポスター） [C3]
横山 陽彦(1), 渡部 卓雄(1) ((1)Tokyo Institute of Technology)
顕在的契約計算への交差型の導入 [C3]
Yuki Nishida(1), Atsushi Igarashi(1) ((1)Kyoto University)
Belief Propagation for Predicate Satisfiability Checking [C3]
Hinata Yanagi(1), Hiroshi Unno(2) ((1)University of Tsukuba (2)University of Tsukuba / RIKEN AIP)
Ordered ChoiceのかわりにCommitted Choiceを用いるGuarded PEGの提案(ポスター) [C3]
小坂 俊介(1), 子原 勇人(1), 前田 敦司(2) ((1)筑波大学情報学群情報科学類 (2)筑波大学システム情報系)
カーネル非依存SIMD化テンプレート [C3]
佐藤 重幸(1) ((1)The University of Tokyo)
グラフ書換え言語における静的型体系LMNtal ShapeTypeの再定式化と拡張（ポスター） [C3]
山本 直輝(1), 上田 和紀(1) ((1)Waseda University)
コーディングスタイルの変遷を統計的に解析するためのデータセットの構築 [C3]
中丸 智貴(1), 千葉 滋(1) ((1)The University of Tokyo)
ジャグ配列を用いるFMO計算の効率的並列化に向けたDSLの設計 (ポスター) [C3]
西田 秀之(1), 千葉 滋(1) ((1)The University of Tokyo)
組込みシステム向けFRP言語の静的スケジューリングを用いた並列化 (ポスター) [C3]
櫻井 義孝(1), 渡部 卓雄(1) ((1)Tokyo Institute of Technology)
OCaml 初学者の syntax error 調査 [C3]
北川 舞(1), 浅井 健一(1) ((1)お茶の水女子大学)
3日目午前の部 (3月8日 9:00-12:50)
9:00-10:00 セッション11 証明支援系 (座長：中澤 巧爾（名古屋大）)
Reasoning with Conditional Probabilities and Joint Distributions in Coq [C1]
Reynald Affeldt(1), Jacques Garrigue(2), Takafumi Saikawa(2) ((1)National Institute of Advanced Industrial Science and Technology (AIST) (2)Nagoya University)
Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS [C2]
山田 麗(1), 浅井 健一(1) ((1)お茶の水女子大学)
shift/reset のための selective CPS 変換の正当性の証明 [C1]
石尾 千晶(1), 浅井 健一(1) ((1)お茶の水女子大学)
10:00-10:20 休憩
10:20-11:20 セッション12 形式言語とその応用 (座長：塚田 武志（東京大学）)
On repetitive right application of B-terms [C2]
Mirai Ikebuchi(1), Keisuke Nakano(2) ((1)MIT, United States (2)Tohoku University)
ランク付き木から文字列への決定性ストリーム変換器の表現力 [C1]
高橋 祐多(1), 中野 圭介(2) ((1)電気通信大学 大学院情報理工学研究科 (2)東北大学)
Moore-Machine Filtering for Timed and Untimed Pattern Matching [C2]
Masaki Waga(1), Ichiro Hasuo(1) ((1)National Institute of Informatics)
11:20-11:40 休憩
11:40-12:20 セッション13 項書換え (座長：山田 晃久（国立情報学研究所）)
書き換え帰納法を利用した帰納的定理証明の補題生成法 [C1]
加藤 裕人(1), 青戸 等人(1) ((1)新潟大学)
決定手続きを用いた項書き換えシステムの帰納的定理自動証明 [C1]
山口 諒(1), 青戸 等人(1) ((1)新潟大学)
12:20-12:50 クロージング

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.