Winter Term 2024/25 Functional Programming with Effects Interactive Theorem Proving Programming Languages 2