|
Praktische Semantik von Programmiersprachen (SemProg)7.5 ECTS (englische Bezeichnung: Practical Semantics of Programming Languages)
Modulverantwortliche/r: Tadeusz Litak Lehrende:
Tadeusz Litak
Start semester: |
SS 2021 | Duration: |
1 semester | Cycle: |
jährlich (SS) |
Präsenzzeit: |
56 Std. | Eigenstudium: |
169 Std. | Language: |
Deutsch und Englisch |
Lectures:
Inhalt:
We study the foundations of the imperative and functional languages, including semantics and type systems. The special feature of this course is that theory is done in a very practical and hands-on way: we not just prove, but program all the results from first-principles. The basic tool used in the course is Coq proof assistant, which can be regarded as a functional programming language in its own right. It has been used, for example, to verify correctness of Java Card technology, C compilers or, more recently, fragments of x86 architecture.
Lernziele und Kompetenzen:
- Wissen
- The students explain the basics of both programming semantics and proof assistants, in particular Coq.
- Verstehen
- The students prove theorems using a proof assistant.
- Anwenden
- The students transfer proofs into programs and programs into proofs.
- Analysieren
- The students examine behaviour of simple programs using formal semantics
- Evaluieren (Beurteilen)
- The students evaluate the role played by logic and type theory in scientific approach to programming.
- Erschaffen
- The students provide formal semantics to a simple programming language.
Literatur:
Online book "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/
Online books by Adam Chlipala: "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ and "Formal Reasoning About Programs" http://adam.chlipala.net/frap/
Supplementary reading on the theory of programming: Types and Programming Languages
Benjamin C. Pierce, The MIT Press
Supplementary reading on Coq: Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
Series: Texts in Theoretical Computer Science. An EATCS Series
Bertot, Yves, Casteran, Pierre
Weitere Informationen:
Keywords: Theorembeweisen Semantik Programmiersprachen
www: http://www8.cs.fau.de/course:semprog
Studien-/Prüfungsleistungen:
Mündliche Prüfung zu Praktische Semantik von Programmiersprachen (Prüfungsnummer: 599478)
(englischer Titel: Practical Semantics of Programming Languages)
- Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, 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 fünf Übungsaufgaben zusammen. Gemäß Corona-Satzung wird als alternative Prüfungsform zur mündlichen Prüfung festgelegt: mündliche elektronische/digitale Distanzprüfung mit 30 Minuten Dauer.
- Prüfungssprache: Deutsch und Englisch
- Erstablegung: SS 2021, 1. Wdh.: WS 2021/2022 (nur für Wiederholer)
|
|
|