Moses - Lambda-Kalkül und Typ-Systeme

Anzeigesprache

Diese Modulbeschreibung gilt nicht im aktuellen Semester.

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

Modul / Version:
#40826 / #1

Gültigkeit:
SS 2017 - SS 2019

Standard-Anzeigesprache:
Deutsch/Englisch

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 Type Systeme erstellt werden, um die Korrektheit funktionaler Programme zu garantieren. Sie können Standard Type Systeme mit verschiedenen Ausdrucksstärken beschreiben und verfügen über ein solides Grundverständnis der möglichen Anwendungsgebiete dieser Type Systeme.

Lehrinhalte

- Lambda-Kalkül (als Berechnungsmodell) - Abstract machines und Auswertungen - Curry-Howard Korrespondenz (Logik / Berechnungnen) - Einfach-getypter und polymorpher Lambda-Kalkül - Theory abhängiger Datentypen - Anwendungen von Type Systemen (z.B. Haskell, Agda) - Typen für Erweiterungen des Lambda-Kalküls

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:

Wünschenswerte Voraussetzungen für die Teilnahme zu den Lehrveranstaltungen: Inhaltlich werden Kenntnisse aus der Theoretischen Informatik zu Logik vorausgesetzt. Verpflichtende Voraussetzungen für die Modulprüfungsanmeldung: keine

Verpflichtende Voraussetzungen für die Modulprüfungsanmeldung:

Dieses Modul hat keine Prüfungsvoraussetzungen.

Abschluss des Moduls

Benotung

benotet

Prüfungsform

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
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