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

井上亜星. Lean でのドキュメント・教科書作成ツール
Kazuki Watanabe and Mayuko Kori. No-Go Theorems for Temporal Verification with Coalgebraic Product Constructions
Jinping Lei, Toru Takisaka, Junqiang Peng and Mingyu Xiao. Parameter Optimization In Approximate Model Counting
伊藤碧己 and 番原睦則. 解集合プログラミングを用いた INRC ナーススケジューリング問題の解法
齊藤哲平 and 廣川直. 重み付き経路順序の一般化を用いた等式の定理自動証明
川野蓮弥 and 結縁祥治. 時間付き可逆プロセス計算 revTPL のシミュレーターツールの実現
脇坂遼 and 鈴木泰成. 格子手術プログラムのためのコンポジショナルな量子ビット割り当て手法
藤原佑輔, 松下祐介, 末永幸平 and 五十嵐淳. 多重配列を扱う命令型プログラムの所有権と篩型を組み合わせによる形式検証
笠浦一海, 水野勇磨, 塚本慧, 恩田直登 and 園田翔. LeanによるRademacher複雑度の形式化に向けて
郡茉友子, 渡邉知樹 and Jurriaan Rot. 到達可能性条件下における始代数の対応
永山充 and 番原睦則. 背景理論付き解集合プログラミングを用いた配電網問題の解法に向けて
神拓己 and 五十嵐淳. eBPFプログラムの機能正当性検証に向けた検証フレームワークの提案
窪寺瑛太郎, 中神悠太 and 中井央. プラグインによってプログラミング言語を自由に構成できるシステムの提案
早川銀河 and 溝口佳寛. DNA計算に関するCoqモジュール開発
名越龍一. 測定型量子計算の形式検証
中村太陽. 量子通信プロトコルのデータベース構築
桂宏行, 小林直樹, 酒寄健 and 佐藤亮介. Catamorphismを用いた代数的データ型を含むプログラムの不変条件の自動合成手法
謝志杰, 笹田耕一, 増原英彦 and 遠藤侑介. 静的プログラム解析によるCRubyにおけるRB_GC_GUARDマクロの過不足検出
平田賢吾 and 塚田武志. 量子スイッチのための高階プログラミング言語の線形論理による型付け
瀧本哲史, 森口草介 and 渡部卓雄. 定理証明支援系のためのライブラリ検索システム作成に向けて
佐藤拓海 and 中澤巧爾. 再帰呼び出しを含む分離論理の部分正当性のための循環証明体系
坂本洸亮, 中丸智貴 and 森畑明昌. .gitignoreファイルの実態調査および冗長性の解消手法の提案
佐藤聡太, 松下祐介, 末永幸平 and 五十嵐淳. 関数型言語のためのHyper Hoare Typeにむけて
両角颯, 山崎徹郎 and 千葉滋. 変数アクセスの挙動を変化させるためのRubyのメタプログラミングの提案
林みなみ, 田邉裕大 and 増原英彦. ライブプログラミング環境Kanonにおけるプログラマの関心事の強調法の提案
久保拓巳 and 戸田貴久. SMTソルバーのAPIファザーMurxlaのカバレッジ改善に向けて
続隼人 and 住井英二郎. Hedged bisimulationの非対称鍵暗号による拡張
吉尾拓真, 田邉裕大 and 増原英彦. 可視化されたデータ構造の編集による対話的プログラム合成手法RefSynの提案
Youyou Cong, Filip Strömbäck and Kazuki Ikemori. Studying Continuations from an Educational Perspective
Yudai Urabe, Guannan Wei and Youyou Cong. Toward Static Analysis for Programs with Effect Handlers by Abstracting Abstract Machines
大河原萌子 and 滝本宗宏. マルチグレイン並列化に基づく帰納論理プログラミングの⾼速化
中丸智貴. Blackbox Fuzzing による .gitignore の解釈の違いの探索
織田幸弘 and 住井英二郎. セキュリティ束の動的拡張が可能なπ計算の型ベース情報流解析
Jessica Belicia Cahyono, 叢悠悠 and 増原英彦. 代数的データ型による情報のモデル化を練習するためのブロック型演習環境
浦中花菜 and 浅井健一. parametricityを用いたcontrol/promptのCPS変換の正当性の証明
穴田直也 and 寺内多智弘. 例を用いた正規表現修正の文字集合一般化における機械学習技術の利用
村瀬唯斗 and 五十嵐淳. Elaborating Lexical Scoping in Multi-Stage Programming
李張帆 and 亀山幸義. Towards Context-Sensitive Parser Combinator with Regular Language Optimization
舟根大喜. ￢ACの相対的無矛盾性証明のIsabelle/ZFによる形式化
岩見宗弘. 一般的な組合せ子の停止性と非基礎ループ性
釘本蓮 and 岩見宗弘. 小学生を対象とした少人数制オンラインScratchプログラミングにおける学習要因の調査と提案
松岡和貴, 南出靖彦 and 佐藤哲也. Isabelle/HOL による差分プライベートなアルゴリズムの安全な実装
窪田唯花 and 浅井健一. shift/resetを含む関数の篩型を使った内部検証
岩田風多, 山崎徹郎 and 千葉滋. コード編集に対して安定した構文木のための安定した Token Interpretation
DAI Feng, HU Yuefeng, Yamazaki Tetsuro and Chiba Shigeru. An extended analysis of the cause of software regressions in Python and JavaScript
中山崇, 松下祐介, 酒寄健 and 小林直樹. メモリ安全性のためのC++オブジェクトモデルのハイレベルな形式化
夏井優太 and 亀山幸義. ステージングを用いた統合言語クエリ処理系の高速化
唐渡巴琉 and 上野雄大. 関数に限定された継続の合成による限定継続の実現の試み
諏訪敬之 and 五十嵐淳. テンソル形状検査のためにコード生成時アサーションを行うステージつき言語とそのIdris風表層言語
岡本祐希 and 篠埜功. Rustにおける不要なクローンを除去する手法の提案および実装
陳智騏, 叢悠悠 and 増原英彦. Towards Live Effectful Programming with Typed Holes
入江堅吾, 和賀正樹 and 末永幸平 . 記号的ミーリオートマトンの能動的学習
Xie Yugu, Dai Feng, Yamazaki Tetsuro and Chiba Shigeru. An Attempt of Combining Natural Language Instructions with Traditional Programming
大倉功士 and 末永幸平. スマートコントラクトのためのファジングのHoare論理による効率化
清水琢也, 酒寄健 and 小林直樹. ポインタの由来に着目したCポインタからRust参照への変換
田村来希, 小谷大祐 and 岡部寿男. スタック上置換を用いた言語仮想マシンのライブマイグレーション
出山翔大 and 池渕未来. 文字列書き換え系における有限導出型の高階への拡張
矢口紘人 and 亀山幸義. 漸進的型付き計算に対する多段階計算の導入
中村元昭 and 佐藤重幸. MN-Core アセンブリ言語の形式検証に向けて
陳沛恩, 田邉裕大, 叢悠悠 and 増原英彦. Adapting Ownership Types for Resource-Safe Algebraic Effect Handling
大志万優生 and 五十嵐淳. 動的型推論を行う漸進的型付け言語のコンパイル手法
山下拓真, 吉岡拓真, 池渕未来 and 今井宜洋. OCamlからEVMバイトコードへのコンパイラ
畠山竜迅 and キセリョーヴオレッグ. Applicativeによるグラフィカルモデルの表現と厳密推論に向けた実装
中神悠太, 中井央 and 三宮秀次. プログラミング言語へのユーザレベル修飾子の導入
眞田嵩大. ニューラルネットワークプログラミング言語のための代数構造
岡慶樹 and 上田和紀. モデリング言語LMNtalによる操作的メモリモデルの表現と検証
内城勇太 and 寺内多智弘. PLMFAの変種における表現力と決定不可能性の分析
吉村友成, 田邉裕大 and 増原英彦. メタトレーシングJITコンパイラを用いた多段階計算の高速化への試み
川本裕輔, 小林賢太朗 and 末永幸平. 仮説検定プログラムのための形式検証ツールStatWhy
IGARASHI Atsushi, ISHIKAWA Yutaka, PARK Sewon and SEKIYAMA Taro. Extending Rabbit towards verified networked systems with user-defined semantics for system calls
岩田文都 and 岩崎英哉. Blocklyに基づくブロック型言語からテキスト型言語への移行支援システム
笹田耕一. RubyにおけるRactorローカルGCにむけて
國吉健路 and 岩崎英哉. Raspberry Pi上のGPU向けディープラーニング最適化フレームワーク
朱光漪 and 浅井健一. 限定継続演算子のための多相な型システム
諸冨速人 and 西田雄気. 定理証明支援系 Coq による RANDAO スマートコントラクトの安全性の検証
齋藤佑貴, 中野圭介, 浅田和之 and 菊池健太郎. Elpiを利用したインタプリタ生成コマンドの実装
Xiu-Heng Hua and Keisuke Nakano. Composing tree transducers to eliminate intermediate data structures
Niu Yue and 関山太郎. Revisiting relational semantics of processes
若杉直椰 and 岩崎英哉. Cerebras CS-2 上のプログラミングを支援する並列スケルトン
竹山祐太郎 and 岩崎英哉. 静的型検査を利用したソフトウェアのセマンティックギャップの解消
松本翼, 渡邉知樹, 末永幸平 and 和賀正樹. Efficient Black-Box Checking with Specification-Guided Abstraction
長田和樹. 双方向変換における１６個のレンズ則の含意関係
熊本航太, 叢悠悠 and 増原英彦. 自然言語を用いてプログラム設計を学ぶ対話型学習環境の開発
川添裕功, 谷口茜, 叢悠悠 and 増原英彦. Algebraic/Scoped effects & handlersの型保存CPS変換
小西京香, 叢悠悠 and 増原英彦. 限定継続の学習支援のための抽象機械に基づく可視化
吉岡拓真, 関山太朗 and 五十嵐淳. 色付き双方向型付けによる型要求フローの定式化
鄭嘉蓉 and 上田和紀. グラフ書換え言語による量子回路の簡単化
松山皓星, 叢悠悠 and 増原英彦. コレオグラフィックプログラミングのエフェクト及びコエフェクトシステムを用いた定式化
野牧樹 and 中井央. ブラウザで実行されるWebアプリケーションのためのJVM
鈴木豪, 渡部卓雄 and 森口草介. 組込みデバイスのメモリ保護ユニットを活用したメモリ管理手法に向けた事前評価
近藤湧太 and 日高宗一郎. 仮想ビューに基づく関係データベースの双方向変換
望月文香, 山崎徹郎 and 千葉滋. BlueScript VM: 非集約型仮想機械による高速かつ省メモリの言語処理系の試作
長谷川咲 and 上田和紀. LMNtalとTamarin Proverを用いたセキュリティプロトコル検証の比較研究
今井敬吾. モナディックなリアクティブシステムの仕様記述におけるReificationの活用に向けて
中村光希, 関山太朗 and 五十嵐淳. CPS 計算の線形型による拡張
山崎徹郎, 山隈由衣 and 千葉滋. Flat-chaining 形式と sub-chaining 形式のどちらでも呼び出せる fluent interface の生成手法のやり直し
川原知真 and 寺内多智弘. 一般化代数的データ型 (GADT) における多相再帰を必要とするプログラムの型推論
糟谷颯希, 田邉裕大 and 増原英彦. 非互換な振る舞いの変更を動的に適用するパッチ作成ための補助機構
野木知優, 中野圭介, 浅田和之, 菊池健太郎 and 佐藤龍之介. 定理証明支援系におけるプロパティベーステストのための網羅的関数生成
武樋一樹, 山崎徹郎 and 千葉滋. 複数再開が可能なエフェクトハンドラのJavaScriptのジェネレータによる実装に向けて
高野保真. SMTソルバZ3の実行結果を用いた他ソルバの性能予測の検討
齋藤匡 and 岩崎英哉. 埋め込み領域特化言語における親言語機能の制限
稲葉亮太, 増原英彦, 田邉裕大 and 叢悠悠. Language Server Protocolを用いたライブプログラミング環境Kanonの汎環境化
松下祐介, 田邉裕大, 関山太朗 and 五十嵐淳. Linear Haskell での Rust 流借用の純粋な実現
田久健人 and 上田和紀. MELL proof netsにおける代入表現の再考
伊藤耀 and 浅田和之. 係数環完備化と貼り合わせ・直交性に基づく線形論理のΣ加群モデルの再構成
小野寺宏介. An Involutory Programming Language
Alessandro Bruni, Reynald Affeldt, Pierre Roux and Takafumi Saikawa. Developing probability theory using the Lebesgue integral in Coq
石井達也 and 木村大輔. 様相μ計算の2つの証明体系TpreとTωの関係
モンタキュートヨアフ. 関係構造上の並行ゲーム

PPL 2025 Accepted Papers/Posters/Demos

カテゴリ１

カテゴリ２

カテゴリ３