Interactive Theorem Proving with Lean

Dieser Kurs konzentriert sich auf interaktives Theorembeweisen, d. h. darauf, wie logische Aussagen in einer formalen, maschinenüberprüfbaren Sprache präzise formuliert werden können, und wie diese Beweise im Lean Theorembeweiser erstellt werden können. Der Kurs legt Focus auf Themen der Informatik, insbesondere die Semantik von Programmiersprachen und Verifikation. Konkret umfasst der Kurs folgende Inhalte: Grundlagen der Typentheorie "Propositions as Types"/die Curry-Howard-Korrespondenz Beweise mit Taktiken Induktive Typen Operationale und denotationale Semantik Programmlogiken Metaprogrammierung