I report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University Munich. The course first intoduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range of standard data structures, in particular search trees and priority queues: it is shown how to express these data structures functionally and how to reason about their correctness and running time in Isabelle.