|
Praktische Semantik von Programmiersprachen (SemProg)7.5 ECTS (englische Bezeichnung: Practical Semantics of Programming Languages)
(Prüfungsordnungsmodul: Praktische Semantik von Programmiersprachen)
Modulverantwortliche/r: Tadeusz Litak Lehrende:
Tadeusz Litak
Startsemester: |
SS 2021 | Dauer: |
1 Semester | Turnus: |
jährlich (SS) |
Präsenzzeit: |
56 Std. | Eigenstudium: |
169 Std. | Sprache: |
Deutsch und Englisch |
Lehrveranstaltungen:
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:
Schlüsselwörter: Theorembeweisen Semantik Programmiersprachen
www: http://www8.cs.fau.de/course:semprog
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
- Artificial Intelligence (Master of Science)
(Po-Vers. 2021s | TechFak | Artificial Intelligence (Master of Science) | Gesamtkonto | Wahlpflichtmodulbereich | Symbolic Artificial Intelligence | Praktische Semantik von Programmiersprachen)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Bachelor of Arts (2 Fächer))", "Informatik (Bachelor of Science)", "Informatik (Master of Science)", "Mathematik (Bachelor of Science)" verwendbar. Details
Studien-/Prüfungsleistungen:
Mündliche Prüfung zu Praktische Semantik von Programmiersprachen (Prüfungsnummer: 599478)
(englischer Titel: Practical Semantics of Programming Languages)
zugeh. "mein campus"-Prüfung: | - 599478 Praktische Semantik von Programmiersprachen (Gewichtung: 100.0 %, Prüfung, Form: mündliche Prüfung, Drittelnoten (mit 4,3), Dauer: -, 7.5 ECTS, Prüfung).
|
- 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)
1. Prüfer: | Tadeusz Litak (100372) |
|
![](/img/anew/void.gif) |
![](/img/anew/void.gif) |
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|