ポスターギャラリー

PPL2025

文字列書き換え系における有限導出型の高階への拡張 出山 翔大, 池渕 未来 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 計算の線形型による拡張 中村 光希, 関山 太朗, 五十嵐 淳
動的型推論を行う漸進的型付け言語のコンパイル手法 大志万 優生, 五十嵐 淳

APLAS2024

(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

RV2024

FalCAuN − CPS Testing with Automata Learning Masaki Waga 最優秀ポスター・ツールショーケース賞受賞

PPL2024

項書換系の完備化を用いたCoqの等式証明プラグイン 矢島 創一, 池渕 未来	代数的エフェクトとハンドラのためのエフェクトシステムの抽象化 吉岡 拓真, 関山 太朗, 五十嵐 淳	モジュールの静的解釈に関するより網羅的かつ堅牢な正当性の証明を目指して 諏訪 敬之, 五十嵐 淳
iCon: Tezos スマートコントラクト群に対する未知の存在する下での協調動作検証器 西田 雄気, 末永 幸平, 五十嵐 淳	データフローセキュリティの検証のための IoT システムモデリング言語 Rabbit 稲葉 皓信, 五十嵐 淳, 石川 裕, 関山 太朗

PPL2023

Java 検証器 Regnant の帰還 小林亮太, 五十嵐淳, 末永幸平

PPL2022

Regnant: 分割可能所有権と篩型を用いた Java 検証器 小林亮太, John Toman, 五十嵐淳, 末永幸平

京都大学 第16回ICTイノベーション

仕様強化を用いたモデル検査による効率的なブラックボックス検査 四十坊純也, 和賀正樹, 末永幸平

PPL2021

レコードとハッシュテーブルの暗黙な相互運用を可能にする型推論とコンパイル手法 梅木孝輔, 関山太朗, 五十嵐淳

暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証 伴野良太郎, 佐藤聡太, 古瀬淳, 末永幸平, 五十嵐淳

物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化 四十坊純也, 和賀正樹, 末永幸平

PPL2020

ReFX: 型に基づくスマートコントラクト自動検証器 陳然, 齋藤大聖, 河田旺, 西田雄気, 五十嵐淳, 末永幸平, 古瀬淳	依存型を備えた多段階計算の同値型による拡張 勝田峻太朗, 五十嵐淳	量子プログラムのための依存型を用いた coupling graph 解析 脇坂 遼, 五十嵐 淳
Homoiconic Lisp 福田陽介	Toward a modalized linear-non-linear model 福田陽介

京都大学 第14回ICTイノベーション

ReFX: 型に基づくスマートコントラクト自動検証器 陳然,齋藤大聖,河田旺,西田雄気,五十嵐淳,末永幸平,古瀬淳

PPL2017

漸進的型付き多相ラムダ計算 五十嵐 雄,関山 太朗,五十嵐 淳

PPL2015

京都大学Teen Racketeer養成コース 五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 宮本 洋平, 大元 武, 末永 幸平 ポスター賞受賞

PPL2014

MapReduce フレームワークにおける Combiner の自動生成 樹下 稔, 末永 幸平, 五十嵐 淳

多段階計算の体系𝜆▷への持ち上げ操作の導入 花田 裕一朗, 五十嵐 淳

PPL2010

プログラムの意味論演習システム 五十嵐淳