PPL 2026: 第28回プログラミングおよびプログラミング言語ワークショップ

Mayuko Kori, Kazuki Watanabe. A No-go Theorem for Coalgebraic Product Construction [29th International Conference on Foundations of Software Science and Computation Structures]
Anton Varonka, Kazuki Watanabe. On Piecewise Affine Reachability with Bellman Operators [50th International Symposium on Mathematical Foundations of Computer Science (MFCS2025)]
Ryota Kojima, Corina Cirstea. Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics [41st Conference on Mathematical Foundations of Programming Semantics MFPS XLI (MFPS 2025)]
Rose Bohrer. Programming Language Case Studies Can Be Deep [Trends in Functional Programming in Education 2024 (TFPiE)]
Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno. Thrust: A Prophecy-based Refinement Type System for Rust [Proceedings of the ACM on Programming Languages, Volume 9, Issue PLDI Article No.: 230, Pages 2056 - 2080]
川本裕輔, 小林賢太朗, 末永幸平. StatWhy: 仮説検定プログラムのための形式検証ツール [The 37th International Conference on Computer Aided Verification (CAV2025)]
Jessica Belicia Cahyono, Youyou Cong, Hidehiko Masuhara. Daisy: An Exercise Environment for Learning Information Modeling [ACM SIGPLAN International Symposium on SPLASH-E (SPLASH-E 2025)]
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi. Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators [ESOP2026: 発表予定]
Mirai Ikebuchi. Homological Invariants of Higher-Order Equational Theories [LICS 2025]
Kayo Tei, Haruto Mishina, Naoki Yamamoto, Kazunori Ueda. Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi [PADL 2026]
Kazutaka Matsuda, Minh Nguyen, Meng Wang. Lenses for Partially-Specified States [ESOP 2026]
Tsubasa Matsumoto, Kazuki Watanabe, Kohei Suenaga, Masaki Waga. Efficient Black-Box Checking with Specification-Guided Abstraction [EMSOFT 2025]
Masaki Waga, Étienne André. Hyper pattern matching [The 25th International Conference on Runtime Verification (RV 2025)]
Takao Yuyama, Ryoma Sin'Ya. Measuring Power of Commutative Group Languages [28th International Conference on Implementation and Application of Automata (CIAA 2024)]
Daisuke Yamaguchi, Shinobu Saito, Takuya Iwatsuka, Nariyoshi Chida, Tachio Terauchi. A Secure Mocking Approach towards Software Supply Chain Security [The 40th IEEE/ACM International Conference on Automated Software Engineering, New Ideas and Emerging Results Track (ASE-NIER 2025)]
Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay, Ichiro Hasuo. Chance and Mass Interpretations of Probabilities in Markov Decision Processes [the 36th International Conference on Concurrency Theory (CONCUR 2025)]
Yoshiki Nakamura. A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead [FoSSaCS 2026]

発表取り下げ
千田忠賢, 山口大輔, 上川先之. Prioritized Streaming String Transducer による逆像計算の高速化
滝坂透, Hongjie Qing, Libo Zhang. On Soundness of Ranking Supermartingales under Weak Non-negativity
佐藤直人, 髙木翼. Maudeによる量子算術演算回路の形式検証
綱島隆太, 中里直人, 鈴木量三朗, 遠藤克浩, 井町宏人, 牧野淳一郎. MN-Core向けOpenACC及びMNCLの言語処理系の開発進展について
殿畑太朗. 拡張パラダイムーー継承とオブジェクト指向を再評価する
石井大輔. A Real-Blasting Extension of cvc5 for Reasoning About Floating-Point Arithmetic
中澤朋, 滝本宗宏. モデル解釈に基づく帰納論理プログラミングの高速化
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka. Solvable Tuple Patterns
田中良尚, 井上裕介. ω-正規言語のzero-one性に対する代数的アプローチ
Kai Pischke, 孫耀珠, 関山太朗. Answer-Type Modification for Lexical Effect Handlers
岡村朋佳, 山本直輝, 上田和紀. グラフ書き換え言語 LMNtal による代数的効果とハンドラのエンコード
橋本拓郎, 塚田武志. 多相的ラムダ計算のモデル検査が決定可能なフラグメントとその応用
小口隼矢, 結縁祥治, 吉田展子, Claudio Antares Mezzina. revGo: Go言語の可逆デバッグに向けた拡張
佐藤拓海, 中澤巧爾. トレース論理のエンテイルメント判定のための循環証明体系
中山祐貴, 寺内多智弘. Delimited Information Release ポリシーの自動合成
井本有哉, 池渕未来. PHOAS を応用した Rocq 上での代数的効果の形式化手法の検討と証明の自動化
森山総太, 井上克巳. グラフアテンションに基づく微分可能なMaxSAT解法
渡邉雄貴, 塚田武志, 鈴木泰成. 高水準記述を扱う誤り耐性量子計算向けコンパイラ
貞本優菜, 結縁祥治. 因果無矛盾的な可逆デバッガCauDErに対する時間意味の導入
Chao GAO. Observer Construction and Opacity Verification Tool for One-Clock Timed Automata
品川拓弥, 住井英二郎. プログラミング言語 Nim の型システムに関する理論的考察
伊澤侑祐, 中丸智貴, 山崎徹郎. Juliaノートブック環境の高速化を目指すアノテーションに基づく編集認識型JITコンパイル手法
神拓己, 和賀正樹, 五十嵐淳, 末永幸平. eBPFプログラムの機能正当性検証のためのモデル検査と実行時検証の統合
福田心美, 浅井健一. Racket と Agda における設計思想および適用領域の比較
清水琢也, 酒寄健, 小林直樹. C/Rust相互運用におけるコンパイラバグのファジングによる探索
須藤龍一, 松田一孝. 高階関数型部分可逆プログラミング言語における配列操作
LIU Yulong, SEKIYAMA Taro. Temporal Algebraic Effect Handlers
諸冨速人, 西田雄気. スマートコントラクトに対するLiveness検証のためのRocqライブラリ
両角颯, 山崎徹郎, 千葉滋. 漸進的借用検査を導入したRust言語のMIRインタプリタによる実現
野牧樹, 中井央, 三宮秀次. WebAssembly 上で動作する言語ランタイムにおけるヒープ外部化アーキテクチャの検討
古賀壮, 小宮常康. WebAssemblyを対象とした基本ブロックバージョニング方式JITコンパイラ
松村陽輝, 上田和紀. グラフ書き換え言語の中間命令列最適化および中間命令内でのバックトラックの削減
桂献一郎, 鍋島英知. 再現性を保証する同期型並列ASPソルバーの設計と実装
Daisuke Yamaguchi, Shinobu Saito, Takuya Iwatsuka, Nariyoshi Chida, Tachio Terauchi. A Secure Mocking Approach towards Software Supply Chain Security
YU HAIXIANG, 和賀正樹. Timed Perception Pattern Matching using Spatial Timed Automata
松本紘周, 山崎徹郎, 千葉滋. LLMを用いたCUDAプログラムの生成の精度向上を目指した修正フィードバックの試作
岡本祐希, 篠埜功. RustOwl: Rustにおける所有権とライフタイムの可視化
佐藤聡太, 松下祐介, 末永幸平, 五十嵐淳. 関数型言語のバグ発見のための篩型システム
榊原麻衣, 山崎徹郎, 千葉滋. プログラム全体を考慮した関数ごとのLLMによるコード生成・修正プログラミングシステムの開発に向けて
片桐健人, 佐藤重幸, 小宮常康. エフェクトハンドラを用いたワークスティーリングの実装
楊恒宇, 李森曦, 戴峰, 山崎徹郎, 千葉滋. Selectively Appending Inferred Type Annotations to Improve the Efficiency of Gradually Typed Programs
坂本洸亮, 山崎徹郎, 千葉滋. サンドボックス的アプローチによるRustにおける循環参照の構築を支援するシステムの試作
名越龍一, 髙木翼. 回路型から測定型への変換と最適化による量子計算の形式検証
岡田大空, 松下祐介, 五十嵐淳. Rustライブラリのスレッド安全性に関するバグのプログラム合成による発見
孫泰昇, 高木翼. 無限長証明を持つ順序ソート条件付き等式論理の到達可能完全性定理
永冨敬士, 小林直樹, 酒寄健. タイムスタンプ付き預言を用いたチャネルに基づく並行プログラムの全自動検証
木下まひな, 南出靖彦. 正規表現マッチングのメモ化アルゴリズムのDafnyによる実装と検証
山下知哉, 上田和紀. ASPソルバー求解可視化ツールの開発
稻吉悠羽, 小林直樹, 酒寄健. 正格性型付けの再考
八木瑛久, 小林直樹, 酒寄健. CHCに基づくWebAssemblyの到達不可能性検証
遠藤侑介. データフロー解析に基づくRuby型解析器の実アプリケーションへの適用と評価
岩田菜々実, 浅井健一. Blocklyへの外部拡張によるOCaml型推論システムの導入とその差分分析
田子内龍介, 住井英二郎. 生成AIを用いた型安全性証明のRocqコード生成
袴田康太, 伊澤侑祐. Forth処理系に対するMeta-tracing JITコンパイラの適用と性能評価
笹倉千楓, 青戸等人. 論理制約付き項書き換えシステムのためのクヌース・ベンディックス順序の提案
近藤湧太, 日高宗一郎. 仮想選択ビュー上の更新操作に対する関数従属性を考慮した基底表への翻訳
鈴木季, 森口草介, 渡部卓雄. リフレクションによる時刻の扱い
Weiyi Zhuang, Akimasa Morihata. Accelerating Data-Intensive Search via a Staged DSL for Effect Handlers
早川銀河, 溝口佳寛. Lean4による関係計算の形式化
朱光漪, 小林直樹, 酒寄健. ニューラルネットワークによる辞書式ランキング関数の合成
柏木力哉, 五十嵐淳. アフィン量子ラムダ計算と双模倣性について
李張帆, 亀山幸義. Monadic Metaprogramming with Bananas, Lenses and Envelopes: A Fusion Framework
藤原佑輔, 松下祐介, 末永幸平, 五十嵐淳. ポインタ演算と多次元配列のための所有権篩型システム
住井英二郎. 非機密化のあるλ計算における型にもとづく安全な情報流のための環境双模倣
桂武蔵, 松下祐介, 小林直樹, 酒寄健. 動的な借用検査を活用したUnsafe Rustコードの正当性検査
鈴木大飛, 青木利晃, TRAN, Duong Dinh. ADS実行時ログデータの可視化による挙動解析
大倉功士, 和賀正樹, 池渕未来, 末永幸平. 摂動付与による麻雀AIの解釈可能性向上
門馬琢磨, Clovis Eberhart, 海野広志. 量的不動点論理を用いた確率的プログラム検証のためのLoop Acceleration
後藤将之, 松下祐介, 五十嵐淳. 型に基づくRust API探索の手法と実装
吉岡拓真, 関山太朗, 五十嵐淳. Unifying Function- and Argument-First Bidirectional Type Systems by Boxy Types
Batyrbek Danel, 亀山幸義. Structuring Böhm-Jacopini Graphs
相馬一葉, 浅井健一. 代数的エフェクトハンドラのSmall-stepインタプリタの導出
山下拓真, 池渕未来. 等式理論に対する有限導出型
Yosuke Fukuda. A categorical semantics of the modal linear lambda-calculus
高杉丈太郎, 中野圭介. 定理証明支援系Rocqにおける述語展開を用いた定理検索プラグインの実装
大塚真太朗. 大規模Rubyアプリケーションに対する自動テスト分散実行基盤
川上竜司, 田邉裕大, 関山太朗. 借用可能リソースのためのTypestateプログラミング
林みなみ, 田邉裕大, 増原英彦. 補助データの構造データへの色付けによる可視化と残像アニメーションの提案
青田紘輝, 小宮常康. CRuby処理系におけるGCガードマクロ漏れによるオブジェクト誤回収の検知手法
秀島宇音, 佐藤重幸, 鵜川始陽. 超並列プロセッサアレイ上のデータベースにおけるオンライン負荷分散に向けて
小高菜摘, 浅井健一. control/promptのsmall-stepインタプリタの導出
足立宏介, 佐藤哲也, 南出靖彦. バックトラックによる後読み付き正規表現マッチングの計算量解析に向けて
洞龍弥, 新屋良磨. 形式言語族上の測度論的な閉包作用素
諏訪敬之, 五十嵐淳. 多段階計算に基づくコンパイル時テンソル形状検査のDNNプログラムへの適用
長谷川光, 五十嵐淳. Rabbitモデルの検証結果における可読性向上のためのトレースグラフの構築
占部雄大. 関数型言語と自然言語における擬引用
松本翼, 渡邉知樹, 和賀正樹. Specification-Guided Abstractionの出力文字列への拡張および確率的モデル検査への応用
石尾千晶, 浅井健一. 限定継続演算子の仮想機械における継続実行の最適化に向けて
北川聖也, 五十嵐淳. ユーザーによる仮定の宣言を可能とするRabbit処理系の拡張と検証の高速化
笠将稀, 岩崎英哉. JavaScriptにおける静的最適化と動的性質の統合と評価
Peien Chen, Yudai Tanabe, Taro Sekiyama. Towards Borrowable Ownership Types with Algebraic Effect Handlers
山内望, 岩崎英哉. JavaScript 処理系におけるオブジェクトへの属性アクセスの最適化
熊本航太, 叢悠悠, 増原英彦. 会話型プログラム設計学習環境Ladderの拡張
瀧本哲史, 森口草介, 渡部卓雄. 同型を除いた単一化を用いた型主導ライブラリ検索
長田和樹, 中野圭介. 定理証明支援系Rocqを用いた双方向変換におけるレンズ則の含意の証明
齋藤佑貴, 中野圭介, 浅田和之, 菊池健太郎. 定理証明支援系による動的型をもつプログラミング言語の検証基盤の実装
吉尾拓真, 田邉裕大, 増原英彦. 直接操作によるデータ構造プログラミングの対話的合成
川浦孟士, 岩崎英哉. IFNライブラリの精度制御機構の改良
谷口茜, Tom Schrijvers, 叢悠悠, 増原英彦. Modular Representation of Choice-Based Computation via Higher-Order Syntax
吉田流晟, 木村大輔. 配列を含む分離論理のエンテイルメント問題とプログラム検証
糟谷颯希, 田邉裕大, 増原英彦. Multi-Version Objectsによる複数バージョンが共存するアプリケーションの構築と進化
磯邊猛, 井上克巳, 杉山麿人. テンソル多体近似を用いた関係データ因子分解の実現
中村光希, 五十嵐淳, 関山太朗. 多相型付きCPS計算および暗黙的多相付きλ計算から多相型付きCPS計算への変換
門脇宗平, 山口悠地, 森口草介, 渡部卓雄. JETLS.jl: 静的解析とランタイム情報を掛け合わせた Julia 言語の高機能 Language Serverの実装
山田龍之介, 中野圭介. 冪等関数のためのプログラミング言語
石黒吉洋. Formalizing the Banach-Zarecki Theorem using Dependent Types
植原一希, 小川広水, Clovis Eberhart, 海野広志. Rustイテレータのためのリファインメント型推論

PPL 2026 Accepted Papers/Posters/Demos

カテゴリ１

カテゴリ２

カテゴリ３

カテゴリ４