Direkt zum Inhalt | Direkt zur Navigation

Sektionen
Benutzerspezifische Werkzeuge

Theorie-Kolloquium

  • Oberseminar, Prof. Dr. Kreitz, Dr. rer. nat. Richter, Di. 14:00-16:00, 3.06.S15

In unserem Kolloquium diskutieren wir aktuelle Forschungsprojekte und -ergebnisse unserer Arbeitsgruppe und für unsere Arbeit relevante Ergebnisse aus den Bereichen Formale Methoden in der Programmierung sowie automatisches und taktikbasiertes Theorembeweisen.

Momentan diskutieren wir ohne individuelle Ankündigungen neuere Arbeiten rund um das faszinierende Thema "Homotopy type theory" resp. "Univalent foundations of mathematics".

Der Fieldspreisträger(2002) Voevodsky hat, aufbauend einerseits auf Ideen aus der algebraischen Homotopietheory und höheren Kategorientheorie, anderseits auf Arbeiten zur Semantik intensionaler Typentheorie von Hofmann/Streicher, Awodey, Warren, van den Berg, Garner und anderen, vorgeschlagen, die Mathematik statt auf Mengen auf Homotpietypen zu gründen. Diese "univalent foundations" versprechen

  • sowohl für klassische als auch für konstruktive Mathematik geeignet zu sein und
  • auf natürliche Weise die inzwischen auch in der theoretischen Informatik allgegenwärtige kategoriale Denkweise zu axiomatisieren.

Möglich wird die Ersetzung der Mengentheorie (die man normalerweise ja schon zur Definition topologischer Räume und Homotopien braucht) allerdings erst durch die erstaunliche Entdeckung, dass Homotopietypen als ein elegantes Modell intensionaler Martin-Löf-Typentheorie aufgefasst werden können.

Wir haben begonnen, den Übersichtsartikel "Type Theory and Homotopy" von Awodey und die Arbeit "The groupoid interpretation of type theory" von Hofmann und Streicher, die als grundlegende Inspiration für die Homotopie-Interpretation von Typentheorie zitiert wird, zu lesen.

Interessierte Zuhörer/Mitstreiter sind herzlich willkommen.

Artikelaktionen
Auf einen Blick
Lehrform Oberseminar
Empfohlen ab FS 6
Voraussetzungen

Aktive Mitarbeit an Themen der Arbeitsgruppe, z.B zur Vorbereitung und Präsentation von Studien- und Abschlussarbeiten. Keine Doppelanrechnung von eigenständiger Leistung.

Benotet Ja
Punkte gesamt 3
davon praktisch 3
Sprache deutsch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000)
Studiengang Bachelor, Master
Modulprüfer Herr Prof.Dr. Christoph Kreitz
Belegung via PULS