jssst sig-ppl

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

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

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

1日目午前の部 (3月6日 9:30-12:15)
9:30-9:35 オープニング
9:35-10:45 セッション1 言語設計 (座長：高野 保真（北里大学）)
Type-based Qubit Allocation for a First-Order Quantum Programming Language [C1]
脇坂 遼(1), 五十嵐 淳(1)((1)Kyoto University)
A Functional Programming Language with Versions [C2]
Yudai Tanabe(1), Luthfan Anshar Lubis(1), Tomoyuki Aotani(2), Hidehiko Masuhara(1)((1)Tokyo Institute of Technology (2)Mamezou)
Sub-chaining style と flat-chaining style 双方の形式に対応した fluent interface 生成に向けた形式的な取り組み [C1]
山崎 徹郎(1), 千葉 滋(1)((1)東京大学)
10:45-11:00 休憩
11:00-12:15 セッション2 論理と証明 (座長：青戸 等人（新潟大学）)
A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates [C1]
益岡 幸弘(1), 木村 大輔(2)((1)総合研究大学院大学 (2)東邦大学)
Biabduction for Separation Logic with Arrays and Lists [C1]
木村 大輔(1), 龍田 真(2), Mahmudul Faisal Al Ameen(3), 池渕 未来(2), 中澤 巧爾(4)((1)東邦大学 (2)NII (3)University of Tokyo (4)名古屋大学)
A Fitch-Style Reconstruction of the Monad-as-Modality Paradigm [C1]
Akinori Maniwa(1)((1)Tokyo Institute of Technology)
1日目午後の部 (3月6日 13:10-20:30)
13:10-13:55 セッション3 形式検証 (座長：江本 健斗（九州工業大学）)
Practical Aspects of Monadic Equational Reasoning in Coq [C1]
Ayumu Saito(1), Reynald Affeldt(2)((1)Tokyo Institute of Technology, School of Computing, Department of Mathematical and Computing Science (2)National Institute of Advanced Industrial Science and Technology (AIST))
Extracting total Amb programs from proofs [C2]
Ulrich Berger(1), Hideki Tsuiki(2)((1)Swansea University (2)Graduate School of Human and Environmental Studies, Kyoto University)
13:55-14:10 休憩
14:10-15:10 セッション4 招待講演(1) (座長：江本 健斗（九州工業大学）)
ブロックチェーンと形式検証 ～ Tezos の場合
古瀬 淳 (ダイラムダ株式会社)
概要 中央管理者のいない分散データベースであるブロックチェーンでは、各サーバノードの運営コストやデータ改竄を防ぐためのインセンティブとして、換金性のあるトークンの導入がどうしても必要になります。結果、ブロックチェーンには巨額の金銭的価値が保持されます。この「お金」との切っても切れない関係、そしてソースコードが全公開されるという性質により、ブロックチェーンシステムに深刻なバグがあった場合、それを突いた巨額のトークン窃盗が起きかねません。このように高い安全性が求められるブロックチェーンでは形式検証は非常に強力な安全化手段となります。 Tezosブロックチェーンでは、安全なシステムの構築を目指しその大きな実装単位である経済プロトコル、プロトコルを使ってブロックの検証を行うシェル、そして契約の自動執行を行うアプリケーションであるスマートコントラクト、それぞれの重要部品に対し実際に形式検証を行っています。本講演ではこれらの検証例のいくつかを紹介します。
15:10-15:25 休憩
15:25-16:30 セッション5 型と形式検証 (座長：中澤 巧爾（名古屋大学）)
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types [C2]
Yuki Nishida(1), Hiromasa Saito(2), Ran Chen(1), Akira Kawata(3), Jun Furuse(2), Kohei Suenaga(1), Atsushi Igarashi(1)((1)Kyoto University (2)DaiLambda, Inc. (3)Preferred Networks, Inc.)
Kmclib: Automated Inference and Verification of Session Types from OCaml Programs [C2]
Keigo Imai(1), Julien Lange(2), Rumyana Neykova(3)((1)Gifu University (2)Royal Holloway, University of London (3)Brunel University)
4種類の限定継続演算子のための型システム [C1]
石尾 千晶(1), 浅井 健一(1)((1)Ochanomizu University)
16:30-16:45 休憩
16:45-18:05 セッション6 ポスター・デモ(1) (座長：新屋 良磨（秋田大学）)
[1] Unified Approach to Program Generation and Verification: A Case Study on Number-Theoretic Transform [C3]
増田 正博(1), 亀山 幸義(1)((1)筑波大学)
[2] Mikiβ における相互再帰の実装 [C3]
大石 美緒(1), 浅井 健一(1)((1)お茶の水女子大学)
[3] 分岐付き確率的プログラミング言語の実現に向けて [C3]
兼光 琢真(1), 関山 太朗(2)((1)総合研究大学院大学 (2)国立情報学研究所)
[4] 高階プロパティ駆動到達可能性 [C3]
桂 宏行(1), 小林 直樹(1), 佐藤 亮介(1)((1)東京大学)
[5] 高階プログラム検証のための所有権型に基づいた可変参照除去 [C3]
Hideto Ueno(1), Naoki Kobayashi(1), Ryosuke Sato(1)((1)The University of Tokyo)
[6] Coq から C への変換器 codegen における借用の実現 [C3]
Akira Tanaka(1)((1)National Institute of Advanced Industrial Science and Technology (AIST))
[7] エラー生成クイズの提案と実施様子の観察結果の紹介 [C3]
角田 和広(1), 増原 英彦(1), 叢 悠悠(1)((1)東京工業大学 情報理工学院 数理・計算科学系)
[8] Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions [C3]
Yeonseok Lee(1), Koji Nakazawa(1)((1)Nagoya University)
[9] 型を利用した音楽自動生成に向けて [C3]
叢 悠悠(1)((1)東京工業大学)
[10] Completeなストリーム融合によるソフトウェア無線のディジタル信号処理 [C3]
小林 友明(1), Oleg Kiselyov(1)((1)Tohoku University)
[11] WebSocket 通信を用いたUniverse フレームワークの拡張 [C3]
上田 結実(1), 浅井 健一(1)((1)お茶の水女子大学)
[12] Proving the correctness of OCaml typing by translation into Coq [C3]
Jacques Garrigue(1), Takafumi Saikawa(1)((1)Nagoya University)
[13] Mizar数学ライブラリの定理検索を行うWebアプリケーション [C3]
Hideharu Furushima(1), Kazuhisa Nakasho(1), Katsumi Wasaki(2)((1)Yamaguchi University (2)Shinshu University)
[14] Goにおけるアクターモデルの実現に向けたライブラリの設計と実装 [C3]
中田 健誠(1), 櫻川 貴司(2)((1)京都大学 総合人間学部 (2)京都大学大学院 人間・環境学研究科)
[15] A design of a dictating programming language for user experience improvement [C3]
Wennong Cai(1), Shigeru Chiba(1)((1)The University of Tokyo)
[16] Kmclib: Automated Inference and Verification of Session Types from OCaml Programs [C3]
Keigo Imai(1), Julien Lange(2), Rumyana Neykova(3)((1)Gifu University (2)Royal Holloway, University of London (3)Brunel University)
[17] Sub-chaining style と flat-chaining style 双方の形式に対応した fluent interface 生成に向けた形式的な取り組み [C3]
山崎 徹郎(1), 千葉 滋(1)((1)東京大学)
18:05-19:30 休憩
19:30-20:30 交流セッション　テーマ「研究室紹介」（何人かの学生さんが，自分の研究室の面白い取り組みなどを紹介してくれます．）
2日目午前の部 (3月7日 9:00-12:10)
9:00-9:45 セッション7 プログラムの理論 (座長：室屋 晃子（京都大学）)
関係プログラム論理のためのモナド上のダイバージェンス [C1]
Tetsuya Sato(1), Shin-Ya Katsumata(2)((1)Tokyo Institute of Technology (2)National Institute of Informatics)
Time-symmetric Turing machines for computable involutions [C2]
Keisuke Nakano(1)((1)Tohoku University)
9:45-9:55 休憩
9:55-10:45 セッション8 エフェクト (座長：叢 悠悠（東京工業大学）)
代数的エフェクトハンドラを持つ言語のためのトレースエフェクト [C1]
川俣 楓河(1), 寺内 多智弘(1)((1)早稲田大学)
代数的エフェクトとハンドラのための CPS 変換と型システム [C1]
藤井 舞花(1), 浅井 健一(1)((1)お茶の水女子大学)
10:45-11:00 休憩
11:00-12:10 セッション9 応用 (座長：宋 剛秀（神戸大学）)
Accelerating XOR-based erasure coding using program optimization techniques [C2]
上里 友弥(1)((1)株式会社ドワンゴ)
PLAGS UT: 自動評価付きPythonプログラミング課題管理システム [C1]
佐藤 重幸(1), 犬伏 貴之(2)((1)東京大学 (2)株式会社シャビセンス)
解集合プログラミングを用いた配電網問題の解法 [C1]
山田 健太郎(1), 湊 真一(2), 田村 直之(3), 番原 睦則(1)((1)名古屋大学 大学院情報学研究科 (2)京都大学 大学院情報学研究科 (3)神戸大学 情報基盤センター)
2日目午後の部 (3月7日 13:10-20:30)
13:10-14:25 セッション10 言語処理系I (座長：前田 敦司（筑波大学）)
フラッシュメモリを持つマイコン向けJavaScript仮想機械の文字列管理 [C1]
近森 凪沙(1), 高田 喜朗(1), 鵜川 始陽(2)((1)高知工科大学 (2)東京大学大学院情報理工学系研究科)
複製に基づく永続化を行うシステムにおける不揮発性メモリ管理手法 [C1]
長安 尚之(1), 鵜川 始陽(2), 松本 康太郎(3), 岩崎 英哉(1)((1)電気通信大学 (2)東京大学 (3)高知工科大学)
ゲストOSのカーネル内メモリへのアクセスを容易にするドメイン特化言語 [C1]
大塚 貴斗(1), 岩崎 英哉(2)((1)電気通信大学 情報理工学域 (2)電気通信大学 大学院情報理工学研究科)
14:25-14:40 休憩
14:40-14:45 スポンサートーク：プラチナスポンサー KLab 株式会社 様
14:45-15:45 セッション11 招待講演(2) (座長：稲葉 一浩（Google）)
静的型つき函数型組版処理システムSATySFiの紹介
諏訪 敬之 (SATySFi開発者)
概要 SATySFi（サティスファイ）は講演者が2017年度のIPA未踏事業の1プロジェクトとして支援のもと開発し，現在も発展を続けている比較的新しい組版処理システムである．SATySFiでは静的型つきのいわゆる函数型言語によってパッケージ或いは文書そのものの一部を書くことができ，一般的なプログラミング言語に近い意味論による高いカスタマイズ性や，型システムによる或る程度原因のわかりやすいエラー報告を実現していることを特徴としている． 本講演では，PPLに参加される方々の興味を鑑みて，特に組版処理や文書作成といった用途に要請されてSATySFiに導入した，意味論や型システム上特徴的な機能について紹介する．講演時点での開発の進展状況によっても紹介できる内容は多少変化しうるものの，主として組版処理特有の組み込み函数がどんな型をもつ定式化になっているかや，（多段階計算やモジュールシステムなどの）より広汎な目的で研究されてきた型システムの理論がどのようにSATySFiで活用されているかについて，デモ等を交えつつ概説したい．
15:45-16:00 休憩
16:00-17:15 セッション12 言語処理系II (座長：日高 宗一郎（法政大学）)
Typed BNF: Backend-independent Semantic Actions [C1]
Taine Zhao(1), Yukiyoshi Kameyama(2)((1)Department of Computer Science, University of Tsukuba (2)University of Tsukuba)
小規模組込みシステム向けFRP言語における非同期タスク処理機構 [C1]
横山 陽彦(1), 森口 草介(1), 渡部 卓雄(1)((1)東京工業大学)
デフォルト値指定機能の導入によるSmPLの拡張 [C1]
山口 大輔(1), 岩塚 卓弥(1)((1)NTTソフトウェアイノベーションセンタ)
17:15-17:25 休憩
17:25-18:45 セッション13 ポスター・デモ(2) (座長：新屋 良磨（秋田大学）)
[18] 型付きのshift/resetを含む言語におけるReflectionに向けて [C3]
山本 充子(1), 浅井 健一(1)((1)お茶の水女子大学)
[19] 参照を用いたデータ構造の形状のユーザ定義の型に基づく型検査 [C3]
佐野 仁(1), 上田 和紀(1)((1)早稲田大学)
[20] WEBフロントエンドにおけるプリプロセッサ言語によるスクリプトの簡略化 [C3]
Tatsuru Tomizawa(1), Shinichiro Yasui(1), Tadashi Okoshi(1), Jin Nakazawa(1)((1)Keio University)
[21] λ計算に対する仕様に基づいたコンパイラの導出 [C3]
横関 茉衣(1), 浅井 健一(2)((1)お茶の水女子大学 (2)Ochanomizu University)
[22] Formalizing quantum circuits with MathComp/Ssreflect [C3]
Takafumi Saikawa(1), Jacques Garrigue(1)((1)Nagoya University)
[23] デザインレシピに基づいた初学者のための学習環境 [C3]
Junya Nose(1), Hidehiko Masuhara(1), Youyou Cong(1)((1)Tokyo Institute of Technology)
[24] グラフ書換え言語LMNtalにおける閉包計算のマッチング最適化 [C3]
今川 連(1), 上田 和紀(1)((1)早稲田大学)
[25] グラフ書き換え言語LMNtalにおけるパーサコンビネータ実装手法 [C3]
山田 啓太(1), 上田 和紀(1)((1)早稲田大学)
[26] 制限された帰納的述語を含む分離論理の完全な循環証明体系 [C3]
石井 沙織(1), 中澤 巧爾(1)((1)名古屋大学大学院情報学研究科)
[27] PLAGS UT: 自動評価付きPythonプログラミング課題管理システム [C3]
佐藤 重幸(1), 犬伏 貴之(2)((1)東京大学 (2)株式会社シャビセンス)
[28] データ駆動文書のためのAPIの改良 [C3]
細部 博史(1)((1)法政大学)
[29] LLVMの中間言語に対するタグ付きunionの検証ツール [C3]
青島 達大(1), 山口 大輔(2), 岩塚 卓弥(2)((1)NTT社会情報研究所 (2)NTTソフトウェアイノベーションセンタ)
[30] OCamlのための構文上の穴を用いたアドホック多相のプリプロセッサによる実装 [C3]
伊藤 将希(1), 今井 敬吾(1)((1)岐阜大学)
[31] 非推奨APIの移行のためのプログラム修正 [C3]
山口 大輔(1), 岩塚 卓弥(1)((1)NTTソフトウェアイノベーションセンタ)
[32] HFL(Z)のための妥当性自動検証手法 [C3]
棚橋 健人(1), 小林 直樹(1), 佐藤 亮介(1)((1)東京大学)
[33] リグレッションテスト生成に向けたプログラム実行履歴の活用 [C3]
石部 大夢(1), 千葉 滋(1)((1)東京大学)
[34] 無限証明体系と循環証明体系の証明能力同等性 [C3]
堀 弘昌(1), 中澤 巧爾(1), 龍田 真(2)((1)名古屋大学 (2)国立情報学研究所)
[35] 不揮発性メモリにオブジェクトの複製を作るJava VMにおけるvolatileフィールドの永続化 [C3]
松本 康太郎(1), 高田 喜朗(1), 鵜川 始陽(2)((1)高知工科大学大学院工学研究科 (2)東京大学大学院情報理工学系研究科)
18:45-19:30 休憩
19:30-20:30 交流セッション　テーマ「プレゼンのコツ」（過去の PPL 発表賞受賞者をお招きして，パネルディスカッションを行います．）
3日目午前の部 (3月8日 9:00-12:15)
9:00-9:50 セッション14 項書換えI (座長：橋本 健二（名古屋大学）)
交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について [C1]
大野 峻(1), 青戸 等人(1)((1)新潟大学大学院自然科学研究科)
危険対条件に基づく条件付き項書き換えシステムの階層可換性 [C1]
芳賀 亮太(1), 青戸 等人(1)((1)新潟大学大学院自然科学研究科)
9:50-10:00 休憩
10:00-10:50 セッション15 項書換えII (座長：菊池 健太郎（東北大学）)
書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合 [C1]
南山 駿人(1), 青戸 等人(1)((1)新潟大学大学院自然科学研究科)
置換に関する不動点制約を用いた名目書き換え [C1]
芳賀 雅樹(1), 青戸 等人(1)((1)新潟大学大学院自然科学研究科)
10:50-11:05 休憩
11:05-12:15 セッション16 多段計算・プログラム合成 (座長：佐藤 重幸（東京大学）)
Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches [C2]
Masaomi Yamaguchi(1), Kazutaka Matsuda(1), Cristina David(2), Meng Wang(2)((1)Graduate School of Information Sciences, Tohoku University (2)University of Bristol)
複数ステージの値が同一ストラクチャのメンバとして共存できる多段階計算のためのモジュールシステム [C1]
諏訪 敬之(1)((1)（民間企業）)
Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus [C1]
勝田 峻太朗(1), 五十嵐 淳(1)((1)京都大学)
3日目午後の部 (3月8日 13:10-17:50)
13:10-14:20 セッション17 正規表現 (座長：中丸 智貴（東京大学）)
Simultaneous Finite Automaton の部分構成による並列正規表現マッチ [C1]
高品 剛大(1), 佐藤 重幸(1), 田浦 健次朗(1)((1)東京大学)
部分語の出現情報の検査のみで近似できる正規言語について [C1]
新屋 良磨(1), 山口 勇太郎(2), 中村 誠希(3)((1)秋田大学 (2)大阪大学 (3)東京工業大学)
Repairing DoS Vulnerability of Real-World Regexes [C2]
Nariyoshi Chida(1), Tachio Terauchi(2)((1)NTT / Waseda University (2)Waseda University)
14:20-14:35 休憩
14:35-15:45 セッション18 プログラミング支援 (座長：今井 敬吾（岐阜大学）)
Is Neural Machine Translation Approach Accurate Enough for Coding Assistance [C2]
Yuka Akinobu(1), Momoka Obara(1), Teruno Kajiura(1), Shiho Takano(1), Miyu Tamura(1), Mayu Tomioka(1), Kimio Kuramitsu(1)((1)Japan Women's University)
型エラープログラムの部分評価 [C1]
対馬 かなえ(1), Robert Glueck(2)((1)国立情報学研究所 (2)The University of Copenhagen)
モジュールをサポートするOCaml ステッパの定式化と実装 [C1]
秋山 雛乃(1), 浅井 健一(1)((1)お茶の水女子大学)
15:45-16:00 休憩
16:00-17:20 セッション19 ポスター・デモ(3) (座長：新屋 良磨（秋田大学）)
[36] CC-PEG: 高速・省メモリな構文解析を実現するPEG方言 [C3]
森田 大樹(1), 松原 寛太(1), 前田 敦司(1)((1)筑波大学)
[37] 部分的な日本語記述からコード候補を提示する統合開発環境に向けて [C3]
髙野 志歩(1), 小原 百々雅(1), 秋信 有花(2), 倉光 君郎(1)((1)日本女子大学 (2)日本女子大学大学院)
[38] 深層学習におけるPython言語モデルの追加事前学習について [C3]
梶浦 照乃(1), 小原 百々雅(1), 秋信 有花(1), 倉光 君郎(1)((1)日本女子大学)
[39] Regnant: 分割可能所有権と篩型を用いた Java 検証器 [C3]
小林 亮太(1), John Toman(2), 五十嵐 淳(1), 末永 幸平(1)((1)京都大学 (2)Certora)
[40] 不揮発性メモリを用いた高い応答性を持つ定期的チェックポインティング [C3]
中田 昌輝(1), 鵜川 始陽(1)((1)東京大学)
[41] 協調性と耐障害性に優れた並列実行順序計画法の改善の検討 [C3]
八杉 昌宏(1)((1)九州工業大学大学院情報工学研究院)
[42] 文脈自由マルチパーティセッション型の実装 [C3]
木村 駿介(1), 今井 敬吾(1)((1)岐阜大学)
[43] 多head左再帰に対応したpackrat parsingアルゴリズムの提案 [C3]
梅田 理生(1), 齋藤 俊哉(2), 依田 純彦(1), 前田 敦司(3)((1)筑波大学 理工情報生命学術院 システム情報工学研究群 情報理工学位プログラム (2)筑波大学 情報学群 情報科学類 (3)筑波大学 システム情報系 情報工学域)
[44] 定理証明支援系Coqを用いたC言語ソートプログラムの検証 [C3]
上西 真由(1), 中野 圭介(1), 浅田 和之(1)((1)東北大学)
[45] OCamlBlocklyのチュートリアル作成 [C3]
柴田 真琴(1), 浅井 健一(1)((1)Ochanomizu University)
[46] 配列言語によるプラズマフラクタル生成アルゴリズムの実装と検討 [C3]
中山 敏宏(1), Oleg Kiselyov(1)((1)Tohoku University)
[47] サイズ情報を伴った再帰データ型を扱う小規模組込みシステム向けFRP言語へのパラメータ多相の導入 [C3]
白井 瑞貴(1), 横山 陽彦(1), 森口 草介(1), 渡部 卓雄(1)((1)東京工業大学)
[48] C/C++上のリモートメモリコンパクションに向けた考察 [C3]
秀島 宇音(1), 佐藤 重幸(1), 田浦 健次朗(1)((1)東京大学)
[49] 組込みシステム向け関数リアクティブプログラムに対するテストケース生成手法 [C3]
内野 駿亮(1), 森口 草介(1), 渡部 卓雄(1)((1)東京工業大学)
[50] 定理証明支援系における型構成の変更に対する証明修復の条件緩和 [C3]
芳賀 勇太(1), 中野 圭介(2), 浅田 和之(2)((1)東北大学情報科学研究科 (2)東北大学電気通信研究所)
[51] 双方向変換プログラミング言語同士の表現力比較 [C3]
宮坂 優介(1), 中野 圭介(2), 浅田 和之(2)((1)東北大学　大学院情報科学研究科 (2)東北大学電気通信研究所)
[52] Formalization of integration theory in Coq [C3]
Reynald Affeldt(1), Cyril Cohen(2)((1)National Institute of Advanced Industrial Science and Technology (AIST) (2)Inria Sophia Antipolis - Méditerrannée)
[53] Fork-Join Parallelism に対する Boehm GC の拡張 [C3]
小林 亮太(1), 椎名 峻平(1), 佐藤 重幸(1), 田浦 健次朗(1)((1)東京大学)
[54] Simultaneous Finite Automaton の部分構成による並列正規表現マッチ [C3]
高品 剛大(1), 佐藤 重幸(1), 田浦 健次朗(1)((1)東京大学)
17:20-17: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. Therefore, presentations in this category, which are informal, should not be considered republication or results of double submissions of any kind.