Introduction to Dependently Typed Programming (IDenT)7.5 ECTS
(englische Bezeichnung: Introduction to Dependently Typed Programming)

Lehrveranstaltungen:

• • Introduction to Dependently Typed Programming
    (Vorlesung mit Übung, 4 SWS, Sergey Goncharov, Mo, 14:15 - 15:45, 02.134-113; Mi, 14:15 - 15:45, 00.131-128)

Empfohlene Voraussetzungen:

Es wird empfohlen, folgende Module zu absolvieren, bevor dieses Modul belegt wird:

Theorie der Programmierung (SS 2021)

Inhalt:

The course provides an introduction to dependently typed programming using Agda as the running programming language for practical exercises. The idea of the course is to present theoretical and practical aspects of dependent type theory through the lens of logic, programming, their connection via the propositions-as-types paradigm and explore the applications of these concepts to functional programming and verification.

Lernziele und Kompetenzen:

Fachkompetenz

Wissen

Students demonstrate an understanding of the role of dependent types and the propositions-as-types paradigm in the context of functional programming and as a semantic mechanism for programming and system specification; Students reproduce the main definitions and results on dependent type semantics and higher order logic, and explain them from a programming perspective.

Anwenden

Students use dependent types to formalise examples, formulate and prove the corresponding verification goals. Students use their theoretic knowledge in dependent type theory for implementing practical problems in concrete programming languages, specifically in Agda.

Analysieren

Students analyse programming challenges, reduce larger tasks to subtasks and correspondingly organise their implementations in a modular fashion, by using the available abstraction mechanisms of dependently typed programming. Students formulate and prove verification goals in a modular way and use interactive mechanisms of the Agda programming environment both to conduct the proofs and to facilitate the development process.

Selbstkompetenz

Students will be regularly provided with small challenges in form of exercises to be able to have a gradual progress with the lecture material.

Literatur:

• Ulf Norell and James Chapman. Dependently Typed Programming in Agda.

• Ana Bove and Peter Dybjer. Dependent Types at Work.

• Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda - A Functional Language with Dependent Types

• Yoshiki Kinoshita. On the Agda Language

• Anton Setzer. Lecture notes on Interactive Theorem Proving.

• Daniel Peebles. Introduction to Agda. Video of talk from the January 2011 Boston Haskell session at MIT.

• Conor McBride. Introduction to Dependently Typed Programming using Agda.

• Andreas Abel. Agda lecture notes.

• Jan Malakhovski. Brutal [Meta]Introduction to Dependent Types in Agda

• Thorsten Altenkirch. Computer Aided Formal Reasoning

• Daniel Licata. Dependently Typed Programming in Agda

• Tesla Ice Zhang. Some books about Formal Verification in Agda (in Chinese)

• Phil Wadler. Programming Languages Foundations in Agda

• Aaron Stump. Verified Functional Programming in Agda

• Diviánszky Péter. Agda Tutorial

• Musa Al-hassy. A slow-paced introduction to reflection in Agda

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Gesamtkonto | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsrichtung Theoretische Informatik | Introduction to Dependently Typed Programming)

Studien-/Prüfungsleistungen:

Introduction to Dependently Typed Programming (Prüfungsnummer: 46401)

(englischer Titel: Introduction to Dependently Typed Programming)

Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 25, benotet, 7.5 ECTS

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Note für die Bearbeitung von 6 Übungsaufgabenblättern zusammen.

Prüfungssprache: Englisch

Erstablegung: SS 2022, 1. Wdh.: WS 2022/2023

1. Prüfer:

Sergey Goncharov