Perlen der Informatik 2
| Dozent: | Prof. Tobias Nipkow |
| Bereich: | Spezialvorlesung im Bachelorstudium: 2 Std. (+2 Ü) |
| Zeit und Ort: | Mi. 8:30 - 10:00 Uhr, MI 00.07.014 |
| Beginn: | 18.4.2012 |
| TUM online |
News
Die Übung findet Donnerstags von 08:30 - 10:00 Uhr in MI 00.11.038 ("John v. Neumann") statt.
Bitte nach Möglichkeit Laptops mitbringen!
Inhalt
In der Vorlesung werden ausgewählte Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen:
- Pratts Primzahlzertifikate
- Logik
- Lambda-Kalkül: ungetypt und einfach getypt.
- Interaktives Beweisen mit Isabelle (5. - ... Woche)
- Haskell
- Zertifizierende Algorithmen
- Endliche Automaten
- Entscheidungsverfahren für Arithmetik
Ziel der Vorlesung ist es, die Studierenden bereits zu Beginn ihres Studiums an Forschungsthemen heranzuführen.
Voraussetzungen: keine
Einen Interpreter für den Lambda-Kalkül gibt es hier.
Unterlagen zu Isabelle
- Programming and Proving in Isabelle/HOL
- Vorlesungsfolien
- Dateien: Overview Nat List Tree Induction Simp Auto_Proof_Demo Single_Step_Demo Inductive_Demo Isar_Demo Isar_Induct_Demo
Proseminar
Ein Teil der Vorlesung findet als Proseminar statt:
Zur Vortragsvorbereitung: How To Present a Paper in Theoretical Computer Science: A Speaker's Guide For Students
Literatur
- Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press.
- John Hughes. Why Functional Programming Matters.
Übungen
| Übungsleitung: | Lars Noschinski |
| Zeit und Ort | Do. 08:30 - 10:00 Uhr, MI 00.11.038 ("John von Neumann") |
| Beginn: | 19.4.2011 |