Perlen der Informatik 3
Dozent: Tobias Nipkow
Übungsleitung: Johannes Hölzl
Details zur Lehrveranstaltung finden sich auf TUM Online. Diese Seite stellt weitere Unterlagen zur Vorlesung und Übung bereit.
News
Inhalt
In der Vorlesung werden Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen. Hier eine Auswahl:
- Logik
- Lambda-Kalkül: ungetypt,
einfach getypt, und
System F und Co.
Online Interpreter für den Lambda-Kalkül - Interaktives Beweisen mit Isabelle
- Cake Cutting Algorithms :-)
- Monaden in Haskell
- Arrow's impossibility theorem: Es gibt kein gerechtes Wahlsystem
- Wie kann man arithmetische Formeln automatisch beweisen?
Ziel der Vorlesung ist es, die Studierenden bereits zu Beginn ihres Studiums an Forschungsthemen heranzuführen.
Voraussetzungen: keine
Unterlagen zu Isabelle
Proseminar
Ein kleiner 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.
Übungen
Zeit und Ort: (Vorraussichtlich) 15:30 - 17:00, John v. Neumann (MI 00.11.038)
- 1. Übung: Blatt 1, Lösung 1
- 2. Übung: Blatt 2
- 3. Übung: Blatt 3
- 4. Übung: Blatt 4, Lösungen: Lambda_Calculus.hs, DeBruijn.hs, Type_Checking.hs.
- 5. Übung: Blatt 5, ex5.thy Isabelle Theorie, Lösung.
- 6. Übung: Blatt 6, ex6.thy Isabelle Theorie.
- 9. Übung: Bit_Tree.thy
- Project: Bit.thy, Bit_Tree.thy