Interaktives Theorembeweisen: Eine Einführung in den Coq-Beweisassistenten
Präsentiert als Teil der Sichere Software-Vorlesung, die 2019 von Martin Leucker am ISP an der Universität zu Lübeck gehalten wurde.
Diese Einführung wurde als Folge von 4 Vorlesungen (jeweils 1,5 Stunden) gehalten, einschließlich einer Einführung in die funktionale Programmierung zu Beginn, für Studierende im 5. Semester. Die Vorlesungen sind so gestaltet, dass sie durch viel Interaktion mit a) den Studierenden und b) dem Beweisassistenten Coq begleitet werden.
