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)