Logik-Sem., 21.06.06, F. Lamarche
Uwe Waldmann
Einladung zum Vortrag
Zeit: Mittwoch, 21.06.06, 14.15 Uhr
Ort: Hörsaal 023, MPI Saarbrücken (Geb. E1.4)
François Lamarche (LORIA Nancy):
What it takes to model dependent types
Zusammenfassung:
The literature on the semantics of dependent type, like the theory
of constructions or Martin-Löf type theory, is highly technical and
uses a large amount of category theory, not all of which is
absolutely necessary.
We will give an elementary approach to this question, which
requires much less abstract baggage: the concept of a display
category (J. Cartmell, 1978). We will take the time to present the
minimal amount of category theory which is necessary for defining
display categories, and give one or two standard examples, like
sets and posets. We will show why something more general is needed,
although display categories do the job most of the time.
______________________________________________________________________
Das Logikseminar ist eine gemeinsame Veranstaltung des DFKI, des MPI
und der Fachrichtungen Informatik, Philosophie und Rechtswissenschaft.
Vortragswünsche bitte an Uwe Waldmann, MPI, Tel.: (0681) 9325-205,
uni-intern: 92205, E-Mail: u...@mpi-sb.mpg.de