Daten
- Anmeldung per StudOn
- Termine und Räume in campo
- Dozent: Thorsten Wißmann
Inhalt
- Was ist ein Beweis?
- Wann ist ein Beweis detailiert genug?
- Im Beweisassistent Agda sind Beweise Programme!
- Aussagen = Typen
- Beweise = Programme
- Beweis-Checker = Compiler
- Damit lassen sich nicht nur Programme schreiben, sondern man kann direkt noch deren Korrektheit zeigen.
- Ziel: am Ende der Veranstaltung können die Teilnehmenden mathematische Sätze und die Korrektheit von algorithmen in Agda beweisen