関数型まつり 2025 で AWS と定理証明について話してきました

DRANK

こんにちは、チェシャ猫です。 先日開催された関数型まつりで、AWS によって開発されたポリシー言語 Cedar と、その開発に使用された定理証明支援系 Lean について登壇してきました。公募 CFP 枠です。 fortee.jp （TODO: 録画が公開されたら貼る） 前回登壇との関係 Cedar については、チェシャ猫自身が少し前、PHPerKaigi 2025 でも登壇しています。 前回と今回では、扱っている題材は同じですが、想定しているターゲットや興味の方向性が少し異なります。今回の登壇では Lean が保証している意味論的な定理や開発フローなど「Cedar がどのように設計・開発され…