Formal Verification 2 The Free-er Monad May 21, 2025 Verified Dynamic Programming with Σ-types in Lean May 21, 2025