Moses - Lambda-Kalkül und Typ-Systeme

Anzeigesprache

Zur Modulseite PDF generieren

Modul / Version:
#40826 / #5

Gültigkeit:
Seit WiSe 2023/24

Standard-Anzeigesprache:
Deutsch

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

Leistungspunkte:
6

Modulverantwortliche*r:
Nestmann, Uwe

Benotung:
benotet

Prüfungsform:
Mündliche Prüfung

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:
TEL 7-2

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

Pflichtgruppe:

Die folgenden Veranstaltungen sind für das Modul obligatorisch:

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

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

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	6	WiSe 2023/24	SoSe 2024
Computer Science (Informatik) (M. Sc.)	1	8	WiSe 2023/24	SoSe 2024
Elektrotechnik (M. Sc.)	1	4	WiSe 2023/24	SoSe 2024
Informatik (B. Sc.)	1	2	WiSe 2023/24	SoSe 2024
Information Systems Management (Wirtschaftsinformatik) (M. Sc.)	1	2	WiSe 2023/24	SoSe 2024

Sonstiges

Keine Angabe