Zur Hauptnavigation Zum Inhaltsbereich Zur Suche Zum Seitenfuß

• TGI
  • Homepage
  • Announcements
• People
  • Staff
  • Students
• Education
  • Education (German only)
  • Thesis (German only)
• Research
• Publications
• Service
  • Service
  • Tools
  • Petri Nets World
    

Titel: Typtheorie

Veranstalter: Mark-Oliver Stehr, Rüdiger Valk

Ort und Zeit: Do 12-14 C-221

Lernziel:

Hauptziel ist das Kennenlernen der theoretischen Grundlagen und der praktische Einsatz der Typtheorie in Hinblick auf Anwendungen in modernen Programmierkonzepten und formalen Beweisen. Ein wesentlicher Bestandteil der Vorlesung sind Übungen mit modernen typtheoretischen Sprachen/Werkzeugen.

Inhalt:

Moderne Typtheorien sind funktionale Programmiersprachen mit extrem ausdruckstarken Typen. Sie liefern eine einfache und einheitliche Sprache zur Repräsentation mathematischer Theorien und Beweise. Programmieren und mathematisches Beweisen fallen unmittelbar zusammen. Typechecking und Proofchecking sind ebenfalls nicht mehr zu trennen. Totale Korrektheit von Programmen/Theoremen wird allein durch Typechecking sichergestellt.

Typentheorien liefern auch eine Grundlage für existierende und zukünf-tige funktionale, objektorientierte und persistente Programmiersprachen/Datenbanken wie z.B. das im AB DBIS entwickelte Tycoon. Typen sind insbesondere relevant bei der (partiellen) Spezifikation von Schnittstellen in Programmiersprachen und verteilten Systemen. Nicht zuletzt sind Typtheorien wichtige Kandidaten für die Basis von komfortablen Beweis-Assistenten der Zukunft, die heutige Computer-Algebra-Systeme um Logik erweitern und somit neue Anwendungsbereiche erschliessen.

Folgende Themen sollen behandelt werden: Ungetyptes und getyptes Lambda-Kalkül (simply typed lambda calculus), System F (second order lambda calculus), Calculus of Constructions (CC), Lambda-Cube (Barendregt), Pure-Type-Systems, Intuitionistische Logik und Curry-Howard-Isomorphismus, Martin Löfs prädikative Typtheorie, Extended Calculus of Constructions (ECC), Calculus of Inductive Constructions (CIC), Einführung in die Werkzeuge LEGO und COQ, Formalisierung elementarer mathematischer Theorien, Einbettung von Logiken (Typtheorie als Logical Framework), Spezifikation/Verifikation von funktionalen, imperativen und parallelen Programmen und nebenläufigen Systemen.

Stellung im Studienplan: Vorlesung im Hauptstudium, Vertiefungsgebiete: Th1, Th2, Th4

Voraussetzung:

Mathematisches Interesse, Geduld und Ausdauer für formales Entwickeln/Beweisen am Rechner

Vorgehen:

Vorlesung mit integrierten Übungen

Literatur:

• Barendregt: Lambda-Calculi with Types, in: Handbook of Logic in Computer Science, Vol. 2, Oxford: Clarendon Press, 1992
• Thompson, Simon: Type Theory and Functional Programming, Addison-Wesley, 1991
• Petersson, K. /Smith, J./Nordström, B.: Programming in Martin Löf's Type Theory. An Introduction. Oxford: Clarendon Press, 1990
• Zhaohui Luo, Computation and Reasoning: A Type Theory for Computer Science. Oxford Univ. Press, 1994.

Periodizität: unregelmäßig

Bemerkungen: Für Lehrer und Nebenfächler nicht geeignet.