Moses - Lambda-Kalkül und Typ-Systeme

Zur Modulseite PDF generieren

Modul / Version
#40826 / #5

Gültigkeit
Seit WiSe 2023/24

Verfügbare Sprache(n)
Deutsch

Titel des Moduls
Lambda-Kalkül und Typ-Systeme

Leistungspunkte
6

Modulverantwortliche*r
Nestmann, Uwe

Benotung
Benotet

Prüfungsform
Mündliche Prüfung

Lehrsprache(n)
Deutsch

Zugehörigkeit

Fakultät
Fakultät IV

Institut
Institut für Softwaretechnik und Theoretische Informatik

Fachgebiet
34351900 FG Modelle und Theorie Verteilter Systeme (MTV)

Prüfungsausschuss
Keine Angabe

Kontakt

Sekretariat
EN 24

Ansprechpartner*in
Nestmann, Uwe

E-Mail-Adresse
uwe.nestmann@tu-berlin.de

Webseite

http://tu.berlin/mtv

Lernergebnisse

Absolventinnen und Absolventen dieses Moduls können Funktionen (mathematische Abstraktion funktionaler Programme) als Terme im Lambda-Kalkül beschreiben. Sie wissen, wie solche Programme abstrahiert und evaluiert werden können. Sie verstehen die Verbindung zwischen logischen Systemen und Berechnungsmodellen und wissen wie Typ-Systeme erstellt werden. Sie können Standard Typ-Systeme mit verschiedenen Ausdrucksstärken beschreiben und verfügen über ein solides Grundverständnis der möglichen Anwendungsgebiete dieser Typ-Systeme.

Lehrinhalte

- Lambda-Kalkül (als Berechnungsmodell): Syntax, Konversion, Auswertung - Einfach getypter und polymorpher Lambda-Kalkül - Typen für Erweiterungen des Lambda-Kalküls: Polymorphie, abhängige Typen - Lambda-Kubus - Curry-Howard Korrespondenz (Logik/Berechnungen) optional: - Abstrakte Maschinen - Anwendungen von Typ-Systemen (z.B. Haskell, Agda)

Modulbestandteile

Pflichtbereich

Die folgenden Veranstaltungen sind für das Modul obligatorisch:

Lehrveranstaltungen	Art	Nummer	Turnus	Sprache	SWS	ISIS	VVZ
Lambda-Kalkül und Typ-Systeme	IV	3435 L 9099	WiSe	Keine Angabe	4

ISIS-Kurssuche nach Veranstaltungen des Moduls

Arbeitsaufwand und Leistungspunkte

Lambda-Kalkül und Typ-Systeme (IV):

Aufwandbeschreibung	Multiplikator	Stunden	Gesamt
Präsenzzeit	15.0	4.0h	60.0h
Prüfungsvorbereitung	1.0	30.0h	30.0h
Studium (Vorbereitungszeit)	15.0	6.0h	90.0h
			180.0h(~6 LP)

Der Aufwand des Moduls summiert sich zu 180.0 Stunden. Damit umfasst das Modul 6 Leistungspunkte.

Beschreibung der Lehr- und Lernformen

Die Veranstaltung folgt der Methode des Inverted Classroom. Studierende bereiten die Inhalte individuell oder in Gruppen zu Hause vor, wobei sie dabei begleitende Fragen und Aufgaben zur Thematik bearbeiten. In der Präsenzzeit werden diese Antworten ausführlich diskutiert, weitere Fragen beantwortet sowie besondere Aufgaben gemeinsam bearbeitet.

Voraussetzungen für die Teilnahme / Prüfung

Wünschenswerte Voraussetzungen für die Teilnahme an den Lehrveranstaltungen:

Kenntnisse und Kompetenzen aus sowie Affinität zu zentralen Bereichen der Theoretischen Informatik, insbesondere Logik.

Verpflichtende Voraussetzungen für die Modulprüfungsanmeldung:

Dieses Modul hat keine Prüfungsvoraussetzungen.

Abschluss des Moduls

Benotung

Benotet

Prüfungsform

Mündliche Prüfung

Sprache(n)

Deutsch, Englisch

Dauer/Umfang

ca. 30 Minuten

Dauer des Moduls

Für Belegung und Abschluss des Moduls ist folgende Semesteranzahl veranschlagt:
1 Semester.

Dieses Modul kann in folgenden Semestern begonnen werden:
Wintersemester.

Maximale teilnehmende Personen

Die maximale Teilnehmerzahl beträgt 25.

Anmeldeformalitäten

Die Teilnahme an der Lehrveranstaltung (nicht zu verwechseln mit der Modulprüfung) wird über einen ISIS-Kurs gesteuert. Die entsprechenden Zugangskoordinaten werden zu Beginn des Moduls bekanntgegeben und 3-4 Wochen lang offen gehalten. Die Anmeldung zur Modulprüfung erfolgt über das Moseskonto. POS-Prüfungsnummer: 2346725

Literaturhinweise, Skripte

Skript in Papierform

Verfügbarkeit: nicht verfügbar

Skript in elektronischer Form

Verfügbarkeit: verfügbar

Literatur

Empfohlene Literatur
Benjamin C. Pierce: Types and Programming Languages. MIT Press, 2002.
Rob Nederpelt and Herman Geuvers: Type Theory and Formal Proof, 2014.

Zugeordnete Studiengänge

Semester:

Zeige auch ausgelaufene Studiengänge und StuPOs

Diese Modulversion wird in folgenden Studiengängen verwendet:

Studiengang / StuPO	StuPOs	Verwendungen	Erste Verwendung	Letzte Verwendung
Computer Engineering (M. Sc.)	1	12	WiSe 2023/24	SoSe 2025
Computer Science (Informatik) (M. Sc.)	1	16	WiSe 2023/24	SoSe 2025
Elektrotechnik (M. Sc.)	1	8	WiSe 2023/24	SoSe 2025
Informatik (B. Sc.)	1	4	WiSe 2023/24	SoSe 2025
Information Systems Management (Wirtschaftsinformatik) (M. Sc.)	1	4	WiSe 2023/24	SoSe 2025

Sonstiges

Keine Angabe