My department (PL and compiler construction) at the University of Kiel, Germany, offers a summer internship in 2020 sponsored by DAAD Rise Germany [1]. The topic of the project is verification of effectful Haskell programs in Coq. For a brief overview of the internship and the topic, please have a look at the project page [2]. We'd be very happy to host a motivated student who likes working with our haskell-to-coq compiler. Depending on personal interests, the focus of the internship can be the compiler itself or its output and the Coq framework for reasoning about the generated code. Previous knowledge of Coq is not required! If you have any questions beforehand, feel free to reply directly or email us at the addresses listed on the project page. The program funding is based on the number of applications, so please spread the news to your colleagues, students or classmates! Best regards, Niels [1] https://www.daad.de/rise/en/rise-germany/find-an-internship/ [2] https://bunkenburg.net/projects/2019-11-01-daad-rise.html