PPL2025 Posters

定理証明支援系のためのライブラリ検索システム作成に向けて（ポスター）

瀧本哲史，森口草介，渡部卓雄
第27回プログラミングおよびプログラミング言語ワークショップ(PPL 2025), Mar. 5-7, 2025.

概要

定理証明支援系を用いる際，プログラミング言語と同様に，既存のライブラリの結果を再利用することで，証明にかかる手間を大きく削減することができる． 再利用を促進するためには，既存のライブラリを横断的かつ網羅的に検索するシステムがあることが望ましい．しかし，RocqやAgda向けのものは構文的にマッチを行うのみで，簡約といった意味論的な側面は考慮しないなど，定理証明支援系向けの検索システムはまだ検索手法が貧弱であると考える． 本発表では，定理証明支援系ではどのような，またどれほど強力な検索が求められているかや，それをどう実現するかなどについて，現段階での研究結果と今後の展望について説明する．

• ポスター

組込みデバイスのメモリ保護ユニットを活用したメモリ管理手法に向けた事前評価（ポスター）

鈴木豪，渡部卓雄，森口草介
第27回プログラミングおよびプログラミング言語ワークショップ(PPL 2025), Mar. 5-7, 2025.

概要

組込みデバイスにはメモリ保護ユニット(Memory Protection Unit)がある． マルチプロセッシング環境においてメモリ保護ユニットを活用した言語処理系はデータの保護やnullチェック以外の目的で利益を享受できる可能性がある． たとえば，メモリ空間の異なるプロセッサ間でデータがやりとりされるとき，リード・ライトバリアを省ける可能性がある． あるいは，計画的にデータの転送を遅延させることで共有バスの応答性低下を軽減し，実時間性の向上が望める可能性がある． 本発表ではその事前準備として，メモリ保護ユニットを活用した場合のレイテンシなどの事前評価をする．

• ポスター