Interactive Theorem Proving: An Intro to the Coq Proof Assistant
Presented as part of the dependable software course taught by Martin Leucker at ISP, Lübeck in 2019.This was given as a series of 4 lectures (each 1.5h), including an intro session to functional programming at the beginning, to undergrad students (5th semester). The lectures are designed to be accompanied by lots of interaction with a) the students and b) the proof assistant Coq.