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 | 


