Ludwig-Maximilians-Universität München, Institut für Informatik
Hauptseminar Kategorielle Logik und Semantik
Inhalt
Denotationelle Semantik erklärt die Bedeutung von Programmen durch Übersetzung in mathematische Modelle. Dabei ist es oft günstig, Modelle innerhalb abstrakter Kategorien zu betrachten und die Übersetzung eines Programms über den Umweg einer dieser Kategorie genau entsprechenden Sprache anzugeben. So entsprechen z.B. funktionale Programmiersprachen dem getypten Lambda Kalkül und haben kartesisch abgeschlossene Kategorien als Modelle. Ziel dieses Seminars ist es, diesen Zusammenhang von Kategorien und ihren zugehörigen Beschreibungssprachen zu untersuchen und eine Verbindung zwischen Programmiersprachen und ihren mathematischen Modellen herzustellen. Dazu sollen u.a. folgende Themen behandelt werden:
- Lawvere-Theorien und Gleichungslogik
- Erweiterung auf Horn-Logik und Prädikatenlogik
- Topoi und intuitionistische Logik
- Kategorien für eine Monade
- computational lambda-calculus.
Eine Einführung in die relevanten Konzepte der Kategorientheorie kann bei Bedarf gegeben werden.
Literatur
- Kock & Reyes: Doctrines in Categorical Logic, In Barwise (ed.), Handbook of Mathematical Logic, North-Holland, 1977.
- Lambek & Scott: Introduction to higher order categorical logic, Cambridge University Press 1986.
- Eugenio Moggi, Notions of Computation and Monads, Information and Computation 93(1), 1991.
- Andrew Pitts, Introduction to Categorical Logic, In: Abramsky et al. (eds.), Handbook of Logics in Computer Science, vol. 6, Oxford, to appear
- (Einführend): A. Poigne, Basic Category Theory. In Abramsky et. al.(eds), Handbook of Logic and Computer Science, vol. 1, Oxford 1992.
Zeit und Ort
Donnerstag, 9.00 Uhr, Raum 033
Sonstiges
Kommentare, Fragen etc. bitte per Email an
Alexander Kurz oder
Dirk Pattinson.
Dirk Pattinson (20/10/1997)