Moses - Lambda-Kalkül und Typ-Systeme

Anzeigesprache

Diese Modulbeschreibung gilt nicht im aktuellen Semester.

Die Modulbeschreibung gilt nur für den Zeitraum WS 2019/20 - WS 2019/20. Die Version für das aktuelle Semester (SoSe 2024) finden Sie hier: Modulbeschreibung des SoSe 2024

Modul / Version:
#40826 / #2

Gültigkeit:
WS 2019/20 - WS 2019/20

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 funktionale Programme mathematisch 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, um die Korrektheit funktionaler Programme zu garantieren. 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) - Abstrakte Maschinen und Auswertungen - Curry-Howard Korrespondenz (Logik/Berechnungen) - Einfach getypter und polymorpher Lambda-Kalkül - Typen für Erweiterungen des Lambda-Kalküls optional: - Theorie abhängiger Datentypen - 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
Hausaufgaben	4.0	15.0h	60.0h
Präsenzzeit	15.0	4.0h	60.0h
Prüfungsvorbereitung	1.0	30.0h	30.0h
Studium (Vor- und Nachbereitung)	15.0	2.0h	30.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 ist betont interaktiv konzipiert. Sie besteht aus einer flexiblen Abfolge von Vorlesungs- und Übungsanteilen. Die Anwendung und Festigung des Stoffs geschieht durch das regelmäßige Bearbeiten von Aufgabenblättern und die Besprechung des Stoffs und der Aufgaben im interaktiven Stil.

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

Dieses Modul ist nicht auf eine Anzahl Studierender begrenzt.

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.

Literaturhinweise, Skripte

Skript in Papierform

Verfügbarkeit: nicht verfügbar

Skript in elektronischer Form

Verfügbarkeit: nicht verfügbar

Literatur

Empfohlene Literatur
Barendregt, H. : Lambda Calculi with Types. 1992
Girard, Jean-Yves : Proofs and Types. Cambridge University Press, 1989.
Hindley, J. Roger : Basic Simple Type Theory. Cambridge Tracts in TCS, 1997.
Martin-Löf, Per : Intuitionistic Type Theory. Bibliopolis, 1984.
Pierce, Benjamin C. : Software Foundations. 2016.
Pierce, Benjamin C. : Types and Programming Languages. MIT Press, 2002.

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
Dieses Modul findet in keinem Studiengang Verwendung.

Sonstiges

Keine Angabe