Proseminar

Übersicht

DatumÄnderungen/Neuigkeiten
19.10.Erstes Treffen auf Donnerstag verschoben
03.11.Treffen mit Themenvergabe

Anforderungen

  • Anwesenheit (keine Fehltermine außer bei attestierter Krankheit)
  • Vorbereitung Expose
  • Diskussion des Exposes mit den Betreuern
  • Vorbereitung Vortragsfolien
  • Vortrag halten

Expose

Die Mitglieder einer Themegruppe arbeiten gemeinsam ein Expose aus. Darin geben sie stichpunktartig die Inhalte an, die in den Vorträgen besprochen werden sollen. Ebenso soll das Expose die Vorträge gegeneinander abgegrenzen. Das Expose soll auch weitere, veröffentlichte Literatur zum Thema angeben und zu jedem gelisteten Paper in 2-3 Sätzen den Zusammenhang erklären. Nach der Sitzung mit dem Betreuer muss das Expose ggf. revidiert werden. Danach können die Vorträge ausgearbeitet werden.

Treffen mit den Betreuern

In der Zeit 8.-22.12.2026.

Vorträge

In der Zeit vom 19.1.-9.2.2027.

Themen

Vier Themenblöcke. Jeweils 3-4 Vorträge pro Block.

Generic Types

  • Paper: Philip Wadler. Theorems for Free!
  • V1: Erklärung des Theorems
  • V2: Beispiel aus Paper formal durcharbeiten
  • V3: Realisierung in Sprachen (Python, Java, TypeScript, Haskell, Scala, …)

Abstract Types

  • Paper 1: John Mitchell, Gordon Plotkin. Abstract Types Have Existential Type.
  • Paper 2: Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism.
  • V1: Grundlagen (P1 / P2)
  • V2: Beispiele (P1 / P2)
  • V3: Realisierung in Sprachen (Python, Java, TypeScript, Haskell, Scala, …)

Traits, Type Classes

  • Paper (Haskell): Philip Wadler, Stephen Blott. How to make ad-hoc polymorphism less ad hoc.
  • Paper (Go): Raymond Hu and others. Welterweight Go: Boxing, Structural Subtyping, and Generics.
  • Paper (Smalltalk): Nathanael Scharli, Stephane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits: Composable Units of Behaviour.

Weitere Möglichkeiten: Scala, Rust, …

Frank Pfenning Lecture Notes on Automated Reasoning

  • imperative programming language semantics
  • how to do correctness proofs
  • logical foundations (dynamic logic)
  • WP (weakest precondition)
  • Lecture-Notes Verzeichnis, relevante Kapitel mit Theorie-Elementen sind Kap. 05 - 11
    • Die konkrete Anwendung bezüglich reg. Ausdrücken ist nicht elementarer Bestandteil (aber evtl. zu Illustrationszwecken geeignet)
    • Ebenso Kap. 04 (Arrays)
    • Die Inhalte zu Why3 sind nicht von Relevanz

Ersatzthemen

[ Metaprogramming, macros, reflection (M4+CPP, Scheme, Lean, MetaML, Scala, …) ] [ Lambda calculus, process calculus (pi, ccs) (translation) ]

Termine

DatumThemaVortragBetreuer