等式理論に対する有限導出型

山下 拓真, 池渕 未来

PHOAS を応用した Rocq 上での代数的効果の形式化手法の検討と証明の自動化

井本 有哉, 池渕 未来

Specification-Guided Abstractionの出力文字列への拡張および確率的モデル検査への応用

松本 翼, 渡邉 知樹, 和賀 正樹

Timed Perception Pattern Matching using Spatial Timed Automata

YU HAIXIANG, 和賀 正樹

摂動付与による麻雀AIの解釈可能性向上

大倉 功士, 和賀 正樹, 池渕 未来, 末永 幸平

eBPFプログラムの機能正当性検証のためのモデル検査と実行時検証の統合

神 拓己, 和賀 正樹, 五十嵐 淳, 末永 幸平

ポインタ演算と多次元配列のための所有権篩型システム

藤原 佑輔, 松下 祐介, 末永 幸平, 五十嵐 淳

関数型言語のバグ発見のための篩型システム

佐藤 聡太, 松下 祐介, 末永 幸平, 五十嵐 淳

Rustライブラリのスレッド安全性に関するバグのプログラム合成による発見

岡田 大空, 松下 祐介, 五十嵐 淳

アフィン量子ラムダ計算と双模倣性について

柏木 力哉, 五十嵐 淳

型に基づくRust API探索の手法と実装

後藤 将之, 松下 祐介, 五十嵐 淳

多段階計算に基づくコンパイル時テンソル形状検査のDNNプログラムへの適用

諏訪 敬之, 五十嵐 淳

Unifying Function- and Argument-First Bidirectional Type Systems by Boxy Types

吉岡 拓真, 関山 太朗, 五十嵐 淳

Rabbitモデルの検証結果における可読性向上のためのトレースグラフの構築

長谷川 光, 五十嵐 淳

ユーザーによる仮定の宣言を可能とするRabbit処理系の拡張と検証の高速化

北川 聖也, 五十嵐 淳

多相型付きCPS計算および暗黙的多相付きλ計算から多相型付きCPS計算への変換

中村 光希, 五十嵐 淳, 関山 太朗

文字列書き換え系における有限導出型の高階への拡張

出山 翔大, 池渕 未来

🏆 PPL 2025 スポンサー特別賞受賞

記号的ミーリオートマトンの能動的学習

入江 堅吾, 和賀 正樹, 末永 幸平

関数型言語のためのHyper Hoare Typeにむけて

佐藤 聡太, 松下 祐介, 末永 幸平, 五十嵐 淳

Extending Rabbit towards verified networked systems with user-defined semantics for system calls

Atsushi Igarashi, Yutaka Ishikawa, Sewon Park, Taro Sekiyama

eBPFプログラムの機能正当性検証に向けた検証フレームワークの提案

神 拓⼰, 五⼗嵐 淳

🏆 PPL 2025 スポンサー特別賞受賞

格子手術プログラムのためのコンポジショナルな量子ビット割り当て手法

脇坂 遼, 鈴木 泰成

多重配列を扱う命令型プログラムの所有権と篩型を組み合わせによる形式検証

藤原 佑輔, 松下 祐介, 末永 幸平, 五十嵐 淳

Linear Haskell での Rust 流借用の純粋な実現

松下 祐介, 田邉 裕大, 関山 太朗, 五十嵐 淳

🏆 PPL2025ポスター賞受賞

⾊付き双⽅向型付けによる型要求フローの形式化

吉岡拓真, 関⼭太朗, 五⼗嵐淳

テンソル形状検査のためにコード生成時アサーションを行うステージつき言語とそのIdris風表層言語

諏訪 敬之, 五十嵐 淳

Efficient Black-Box Checking with Specification-Guided Abstraction

松本 翼, 渡邉 知樹, 末永 幸平, 和賀 正樹

スマートコントラクトのためのファジングのHoare論理による効率化

大倉 功士, 末永 幸平

OCamlからEVMバイトコードへのコンパイラ

山下 拓真, 吉岡 拓真, 池渕 未来, 今井 宜洋

Elaborating Lexical Scoping in Multi-Stage Programming

村瀬 唯斗, 五十嵐 淳

CPS 計算の線形型による拡張

中村 光希, 関山 太朗, 五十嵐 淳

動的型推論を行う漸進的型付け言語のコンパイル手法

大志万 優生, 五十嵐 淳

(Bi-)3 directional Typing for Answer Type Modification

Takuma Yoshioka

🏆 Audience award 受賞

Refined^2 Environment Classifiers

Yuito Murase

🏆 SRC 1st prize および Audience award 受賞

Lightweight Dependent Types via Staging: Compile-Time Manifest Contracts

Takashi Suwa

Towards Ownership Refinement Type Inference with Nested Arrays

Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, Atsushi Igarashi

FalCAuN − CPS Testing with Automata Learning

Masaki Waga

🏆 最優秀ポスター・ツールショーケース賞受賞

項書換系の完備化を用いたCoqの等式証明プラグイン

矢島 創一, 池渕 未来

代数的エフェクトとハンドラのためのエフェクトシステムの抽象化

吉岡 拓真, 関山 太朗, 五十嵐 淳

モジュールの静的解釈に関するより網羅的かつ堅牢な正当性の証明を目指して

諏訪 敬之, 五十嵐 淳

iCon: Tezos スマートコントラクト群に対する未知の存在する下での協調動作検証器

西田 雄気, 末永 幸平, 五十嵐 淳

データフローセキュリティの検証のための IoT システムモデリング言語 Rabbit

稲葉 皓信, 五十嵐 淳, 石川 裕, 関山 太朗

Java 検証器 Regnant の帰還

小林亮太, 五十嵐淳, 末永幸平

Regnant: 分割可能所有権と篩型を用いた Java 検証器

小林亮太, John Toman, 五十嵐淳, 末永幸平

仕様強化を用いたモデル検査による効率的なブラックボックス検査

四十坊純也, 和賀正樹, 末永幸平

レコードとハッシュテーブルの暗黙な相互運用を可能にする型推論とコンパイル手法

梅木孝輔, 関山太朗, 五十嵐淳

暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証

伴野良太郎, 佐藤聡太, 古瀬淳, 末永幸平, 五十嵐淳

物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化

四十坊純也, 和賀正樹, 末永幸平

ReFX: 型に基づくスマートコントラクト自動検証器

陳然, 齋藤大聖, 河田旺, 西田雄気, 五十嵐淳, 末永幸平, 古瀬淳

依存型を備えた多段階計算の同値型による拡張

勝田峻太朗, 五十嵐淳

量子プログラムのための依存型を用いた coupling graph 解析

脇坂 遼, 五十嵐 淳

Homoiconic Lisp

福田陽介

Toward a modalized linear-non-linear model

福田陽介

ReFX: 型に基づくスマートコントラクト自動検証器

陳然,齋藤大聖,河田旺,西田雄気,五十嵐淳,末永幸平,古瀬淳

漸進的型付き多相ラムダ計算

五十嵐 雄,関山 太朗,五十嵐 淳

京都大学Teen Racketeer養成コース

五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 宮本 洋平, 大元 武, 末永 幸平

🏆 ポスター賞受賞

MapReduce フレームワークにおける Combiner の自動生成

樹下 稔, 末永 幸平, 五十嵐 淳

多段階計算の体系𝜆▷への持ち上げ操作の導入

花田 裕一朗, 五十嵐 淳

プログラムの意味論演習システム

五十嵐淳